ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : M →ₗ[R] M<VAR>g : N →ₗ[R] N<VAR>n : ℕ<GOAL>TensorProduct.map f g ^ n = TensorProduct.map (f ^ n) (g ^ n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f₁ f₂ : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>TensorProduct.map (f₁ + f₂) g = TensorProduct.map f₁ g + TensorProduct.map f₂ g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M →ₗ[R] P<VAR>g₁ g₂ : N →ₗ[R] Q<GOAL>TensorProduct.map f (g₁ + g₂) = TensorProduct.map f g₁ + TensorProduct.map f g₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>r : R<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>TensorProduct.map (r • f) g = r • TensorProduct.map f g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>r : R<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>TensorProduct.map f (r • g) = r • TensorProduct.map f g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>((TensorProduct.mapBilinear R M N P Q) f) g = TensorProduct.map f g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R P<VAR>Module R Q<VAR>p : P<VAR>f : M →ₗ[R] Q<VAR>m : M<GOAL>((TensorProduct.lTensorHomToHomLTensor R M P Q) (p ⊗ₜ[R] f)) m = p ⊗ₜ[R] f m
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R P<VAR>Module R Q<VAR>f : M →ₗ[R] P<VAR>q : Q<VAR>m : M<GOAL>((TensorProduct.rTensorHomToHomRTensor R M P Q) (f ⊗ₜ[R] q)) m = f m ⊗ₜ[R] q
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>(TensorProduct.homTensorHomMap R M N P Q) (f ⊗ₜ[R] g) = TensorProduct.map f g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>AddCommMonoid T<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>Module R T<VAR>f : M →ₗ[R] P →ₗ[R] Q<VAR>g : N →ₗ[R] S →ₗ[R] T<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.map₂ f g) (m ⊗ₜ[R] n) = TensorProduct.map (f m) (g n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : N →ₗ[R] Q<GOAL>TensorProduct.map 0 g = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M →ₗ[R] P<GOAL>TensorProduct.map f 0 = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M ≃ₗ[R] P<VAR>g : N ≃ₗ[R] Q<VAR>m : M<VAR>n : N<GOAL>(TensorProduct.congr f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M ≃ₗ[R] P<VAR>g : N ≃ₗ[R] Q<VAR>p : P<VAR>q : Q<GOAL>(TensorProduct.congr f g).symm (p ⊗ₜ[R] q) = f.symm p ⊗ₜ[R] g.symm q
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M ≃ₗ[R] P<VAR>g : N ≃ₗ[R] Q<GOAL>(TensorProduct.congr f g).symm = TensorProduct.congr f.symm g.symm
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>TensorProduct.congr (LinearEquiv.refl R M) (LinearEquiv.refl R N) = LinearEquiv.refl R (TensorProduct R M N)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>AddCommMonoid T<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>Module R T<VAR>f : M ≃ₗ[R] P<VAR>g : N ≃ₗ[R] Q<VAR>f' : P ≃ₗ[R] S<VAR>g' : Q ≃ₗ[R] T<GOAL>TensorProduct.congr (f ≪≫ₗ f') (g ≪≫ₗ g') = TensorProduct.congr f g ≪≫ₗ TensorProduct.congr f' g'
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : M ≃ₗ[R] M<VAR>g : N ≃ₗ[R] N<VAR>f' : M ≃ₗ[R] M<VAR>g' : N ≃ₗ[R] N<GOAL>TensorProduct.congr (f * f') (g * g') = TensorProduct.congr f g * TensorProduct.congr f' g'
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : M ≃ₗ[R] M<VAR>g : N ≃ₗ[R] N<VAR>n : ℕ<GOAL>TensorProduct.congr f g ^ n = TensorProduct.congr (f ^ n) (g ^ n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : M ≃ₗ[R] M<VAR>g : N ≃ₗ[R] N<VAR>n : ℤ<GOAL>TensorProduct.congr f g ^ n = TensorProduct.congr (f ^ n) (g ^ n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>m : M<VAR>n : N<VAR>p : P<GOAL>(TensorProduct.leftComm R M N P) (m ⊗ₜ[R] n ⊗ₜ[R] p) = n ⊗ₜ[R] m ⊗ₜ[R] p
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>m : M<VAR>n : N<VAR>p : P<GOAL>(TensorProduct.leftComm R M N P).symm (n ⊗ₜ[R] m ⊗ₜ[R] p) = m ⊗ₜ[R] n ⊗ₜ[R] p
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>m : M<VAR>n : N<VAR>p : P<VAR>q : Q<GOAL>(TensorProduct.tensorTensorTensorComm R M N P Q) ((m ⊗ₜ[R] n) ⊗ₜ[R] p ⊗ₜ[R] q) = (m ⊗ₜ[R] p) ⊗ₜ[R] n ⊗ₜ[R] q
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<GOAL>(TensorProduct.tensorTensorTensorComm R M N P Q).symm = TensorProduct.tensorTensorTensorComm R M P N Q
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>m : M<VAR>n : N<VAR>p : P<VAR>q : Q<GOAL>(TensorProduct.tensorTensorTensorAssoc R M N P Q) ((m ⊗ₜ[R] n) ⊗ₜ[R] p ⊗ₜ[R] q) = (m ⊗ₜ[R] n ⊗ₜ[R] p) ⊗ₜ[R] q
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>m : M<VAR>n : N<VAR>p : P<VAR>q : Q<GOAL>(TensorProduct.tensorTensorTensorAssoc R M N P Q).symm ((m ⊗ₜ[R] n ⊗ₜ[R] p) ⊗ₜ[R] q) = (m ⊗ₜ[R] n) ⊗ₜ[R] p ⊗ₜ[R] q
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>(LinearMap.lTensor M f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N →ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>(LinearMap.rTensor M f) (n ⊗ₜ[R] m) = f n ⊗ₜ[R] m
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N →ₗ[R] P<VAR>m : M<GOAL>LinearMap.lTensor M f ∘ₗ (TensorProduct.mk R M N) m = (TensorProduct.mk R M P) m ∘ₗ f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N →ₗ[R] P<VAR>m : M<GOAL>LinearMap.rTensor M f ∘ₗ (TensorProduct.mk R N M).flip m = (TensorProduct.mk R P M).flip m ∘ₗ f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : N →ₗ[R] P<GOAL>↑(TensorProduct.comm R P Q) ∘ₗ LinearMap.rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N) = LinearMap.lTensor Q g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : N →ₗ[R] P<GOAL>↑(TensorProduct.comm R Q P) ∘ₗ LinearMap.lTensor Q g ∘ₗ ↑(TensorProduct.comm R N Q) = LinearMap.rTensor Q g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N →ₗ[R] P<GOAL>Function.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑(LinearMap.rTensor M f)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N →ₗ[R] P<GOAL>Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Surjective ⇑(LinearMap.rTensor M f)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N →ₗ[R] P<GOAL>Function.Bijective ⇑(LinearMap.lTensor M f) ↔ Function.Bijective ⇑(LinearMap.rTensor M f)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<GOAL>⇑(LinearMap.lTensorHom M) = LinearMap.lTensor M
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<GOAL>⇑(LinearMap.rTensorHom M) = LinearMap.rTensor M
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f g : N →ₗ[R] P<GOAL>LinearMap.lTensor M (f + g) = LinearMap.lTensor M f + LinearMap.lTensor M g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f g : N →ₗ[R] P<GOAL>LinearMap.rTensor M (f + g) = LinearMap.rTensor M f + LinearMap.rTensor M g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<GOAL>LinearMap.lTensor M 0 = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<GOAL>LinearMap.rTensor M 0 = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>r : R<VAR>f : N →ₗ[R] P<GOAL>LinearMap.lTensor M (r • f) = r • LinearMap.lTensor M f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>r : R<VAR>f : N →ₗ[R] P<GOAL>LinearMap.rTensor M (r • f) = r • LinearMap.rTensor M f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : P →ₗ[R] Q<VAR>f : N →ₗ[R] P<GOAL>LinearMap.lTensor M (g ∘ₗ f) = LinearMap.lTensor M g ∘ₗ LinearMap.lTensor M f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : P →ₗ[R] Q<VAR>f : N →ₗ[R] P<VAR>x : TensorProduct R M N<GOAL>(LinearMap.lTensor M (g ∘ₗ f)) x = (LinearMap.lTensor M g) ((LinearMap.lTensor M f) x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : P →ₗ[R] Q<VAR>f : N →ₗ[R] P<GOAL>LinearMap.rTensor M (g ∘ₗ f) = LinearMap.rTensor M g ∘ₗ LinearMap.rTensor M f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : P →ₗ[R] Q<VAR>f : N →ₗ[R] P<VAR>x : TensorProduct R N M<GOAL>(LinearMap.rTensor M (g ∘ₗ f)) x = (LinearMap.rTensor M g) ((LinearMap.rTensor M f) x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f g : Module.End R N<GOAL>LinearMap.lTensor M (f * g) = LinearMap.lTensor M f * LinearMap.lTensor M g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f g : Module.End R N<GOAL>LinearMap.rTensor M (f * g) = LinearMap.rTensor M f * LinearMap.rTensor M g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>LinearMap.lTensor M LinearMap.id = LinearMap.id
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>x : TensorProduct R M N<GOAL>(LinearMap.lTensor M LinearMap.id) x = x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<GOAL>LinearMap.rTensor M LinearMap.id = LinearMap.id
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>x : TensorProduct R N M<GOAL>(LinearMap.rTensor M LinearMap.id) x = x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>r : R<GOAL>LinearMap.lTensor M (DistribMulAction.toLinearMap R N r) = DistribMulAction.toLinearMap R (TensorProduct R M N) r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>r : R<GOAL>LinearMap.rTensor M (DistribMulAction.toLinearMap R N r) = DistribMulAction.toLinearMap R (TensorProduct R N M) r
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : N →ₗ[R] R<GOAL>↑(TensorProduct.lid R M) ∘ₗ LinearMap.rTensor M f = TensorProduct.lift (LinearMap.lsmul R M ∘ₗ f)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>LinearMap.lTensor P g ∘ₗ LinearMap.rTensor N f = TensorProduct.map f g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>LinearMap.rTensor Q f ∘ₗ LinearMap.lTensor M g = TensorProduct.map f g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<VAR>f' : S →ₗ[R] M<GOAL>TensorProduct.map f g ∘ₗ LinearMap.rTensor N f' = TensorProduct.map (f ∘ₗ f') g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<VAR>g' : S →ₗ[R] N<GOAL>TensorProduct.map f g ∘ₗ LinearMap.lTensor M g' = TensorProduct.map f (g ∘ₗ g')
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>f' : P →ₗ[R] S<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>LinearMap.rTensor Q f' ∘ₗ TensorProduct.map f g = TensorProduct.map (f' ∘ₗ f) g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>AddCommMonoid S<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>Module R S<VAR>g' : Q →ₗ[R] S<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<GOAL>LinearMap.lTensor P g' ∘ₗ TensorProduct.map f g = TensorProduct.map f (g' ∘ₗ g)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : M →ₗ[R] M<VAR>n : ℕ<GOAL>LinearMap.rTensor N f ^ n = LinearMap.rTensor N (f ^ n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>f : N →ₗ[R] N<VAR>n : ℕ<GOAL>LinearMap.lTensor M f ^ n = LinearMap.lTensor M (f ^ n)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N ≃ₗ[R] P<GOAL>↑(LinearEquiv.lTensor M f) = LinearMap.lTensor M ↑f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N ≃ₗ[R] P<GOAL>↑(LinearEquiv.lTensor M f).symm = LinearMap.lTensor M ↑f.symm
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N ≃ₗ[R] P<GOAL>↑(LinearEquiv.rTensor M f) = LinearMap.rTensor M ↑f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N ≃ₗ[R] P<GOAL>↑(LinearEquiv.rTensor M f).symm = LinearMap.rTensor M ↑f.symm
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N ≃ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>(LinearEquiv.lTensor M f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N ≃ₗ[R] P<VAR>m : M<VAR>p : P<GOAL>(LinearEquiv.lTensor M f).symm (m ⊗ₜ[R] p) = m ⊗ₜ[R] f.symm p
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N ≃ₗ[R] P<VAR>m : M<VAR>n : N<GOAL>(LinearEquiv.rTensor M f) (n ⊗ₜ[R] m) = f n ⊗ₜ[R] m
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : N ≃ₗ[R] P<VAR>m : M<VAR>p : P<GOAL>(LinearEquiv.rTensor M f).symm (p ⊗ₜ[R] m) = f.symm p ⊗ₜ[R] m
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : N ≃ₗ[R] P<GOAL>TensorProduct.comm R Q N ≪≫ₗ LinearEquiv.rTensor Q g ≪≫ₗ TensorProduct.comm R P Q = LinearEquiv.lTensor Q g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : N ≃ₗ[R] P<GOAL>TensorProduct.comm R N Q ≪≫ₗ LinearEquiv.lTensor Q g ≪≫ₗ TensorProduct.comm R Q P = LinearEquiv.rTensor Q g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : P ≃ₗ[R] Q<VAR>f : N ≃ₗ[R] P<GOAL>LinearEquiv.lTensor M (f ≪≫ₗ g) = LinearEquiv.lTensor M f ≪≫ₗ LinearEquiv.lTensor M g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>AddCommMonoid Q<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>Module R Q<VAR>g : P ≃ₗ[R] Q<VAR>f : N ≃ₗ[R] P<VAR>x : TensorProduct R M N<GOAL>(LinearEquiv.lTensor M (f ≪≫ₗ g)) x = (LinearEquiv.lTensor M g) ((LinearEquiv.lTensor M f) x)