R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.102460
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_5
N₂ : Type u_6
N : Type u_7
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
x₁ : M₁
x₂ : M₂
⊢ ↑(LinearMap.comp (↑(equiv hg)) (LinearMap.comp (TensorProduct.map i₁ i₂) ↑(LinearEquiv.symm (equiv hf))))
      (↑(↑f x₁) x₂) =
    ↑(↑g (↑i₁ x₁)) (↑i₂ x₂)
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.102460
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_5
N₂ : Type u_6
N : Type u_7
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
x₁ : M₁
x₂ : M₂
⊢ ↑(map hf hg i₁ i₂) (↑(↑f x₁) x₂) = ↑(↑g (↑i₁ x₁)) (↑i₂ x₂)
delta IsTensorProduct.map
no goals
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type ?u.102460
inst✝¹³ : AddCommMonoid M₁
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M₁
inst✝⁸ : Module R M₂
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_5
N₂ : Type u_6
N : Type u_7
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
x₁ : M₁
x₂ : M₂
⊢ ↑(LinearMap.comp (↑(equiv hg)) (LinearMap.comp (TensorProduct.map i₁ i₂) ↑(LinearEquiv.symm (equiv hf))))
      (↑(↑f x₁) x₂) =
    ↑(↑g (↑i₁ x₁)) (↑i₂ x₂)
simp