R : Type u_2
A : Type u_3
B : Type u_4
S : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
a : A
b : B
⊢ ↑(AlgHom.comp
          (algHomOfLinearMapTensorProduct (LinearMap.mul' R S)
            (_ : ∀ (a₁ a₂ b₁ b₂ : S), a₁ * a₂ * (b₁ * b₂) = a₁ * b₁ * (a₂ * b₂))
            (_ : ∀ (r : R), ↑(algebraMap R S) r * 1 = ↑(algebraMap R S) r))
          (map f g))
      (a ⊗ₜ[R] b) =
    ↑f a * ↑g b
R : Type u_2
A : Type u_3
B : Type u_4
S : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
a : A
b : B
⊢ ↑(productMap f g) (a ⊗ₜ[R] b) = ↑f a * ↑g b
unfold productMap lmul'
no goals
R : Type u_2
A : Type u_3
B : Type u_4
S : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
a : A
b : B
⊢ ↑(AlgHom.comp
          (algHomOfLinearMapTensorProduct (LinearMap.mul' R S)
            (_ : ∀ (a₁ a₂ b₁ b₂ : S), a₁ * a₂ * (b₁ * b₂) = a₁ * b₁ * (a₂ * b₂))
            (_ : ∀ (r : R), ↑(algebraMap R S) r * 1 = ↑(algebraMap R S) r))
          (map f g))
      (a ⊗ₜ[R] b) =
    ↑f a * ↑g b
simp