Loogle!

Result

Found 938 declarations mentioning LinearMap and TensorProduct. Of these, only the first 200 are shown.

• TensorProduct.Neg.aux 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] : TensorProduct R M N →ₗ[R] TensorProduct R M N
• LinearMap.lTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : TensorProduct R M N →ₗ[R] TensorProduct R M P
• LinearMap.rTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : TensorProduct R N M →ₗ[R] TensorProduct R P M
• LinearMap.lTensor_id 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : LinearMap.lTensor M LinearMap.id = LinearMap.id
• LinearMap.rTensor_id 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : LinearMap.rTensor M LinearMap.id = LinearMap.id
• TensorProduct.map 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : TensorProduct R M N →ₗ[R] TensorProduct R P Q
• TensorProduct.map_id 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : TensorProduct.map LinearMap.id LinearMap.id = LinearMap.id
• LinearMap.lTensor_def 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : LinearMap.lTensor M f = TensorProduct.map LinearMap.id f
• LinearMap.rTensor_def 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : LinearMap.rTensor M f = TensorProduct.map f LinearMap.id
• LinearMap.lTensor.eq_1 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : LinearMap.lTensor M f = TensorProduct.map LinearMap.id f
• LinearMap.rTensor.eq_1 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : LinearMap.rTensor M f = TensorProduct.map f LinearMap.id
• TensorProduct.lift_mk 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : TensorProduct.lift (TensorProduct.mk R M N) = LinearMap.id
• TensorProduct.liftAux 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) : TensorProduct R M N →+ P
• TensorProduct.curry 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) : M →ₗ[R] N →ₗ[R] P
• TensorProduct.lift 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) : TensorProduct R M N →ₗ[R] P
• TensorProduct.curry_injective 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : Function.Injective TensorProduct.curry
• TensorProduct.mapOfCompatibleSMul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (A : Type u_4) (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [TensorProduct.CompatibleSMul R A M N] : TensorProduct A M N →ₗ[A] TensorProduct R M N
• LinearMap.lTensor_id_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) : (LinearMap.lTensor M LinearMap.id) x = x
• LinearMap.rTensor_id_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R N M) : (LinearMap.rTensor M LinearMap.id) x = x
• TensorProduct.mk 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : M →ₗ[R] N →ₗ[R] TensorProduct R M N
• LinearMap.lTensor_smul_action 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r : R) : LinearMap.lTensor M (DistribMulAction.toLinearMap R N r) = DistribMulAction.toLinearMap R (TensorProduct R M N) r
• LinearMap.rTensor_smul_action 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r : R) : LinearMap.rTensor M (DistribMulAction.toLinearMap R N r) = DistribMulAction.toLinearMap R (TensorProduct R N M) r
• LinearEquiv.coe_lTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : ↑(LinearEquiv.lTensor M f) = LinearMap.lTensor M ↑f
• LinearEquiv.coe_rTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : ↑(LinearEquiv.rTensor M f) = LinearMap.rTensor M ↑f
• TensorProduct.mapOfCompatibleSMul' 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (A : Type u_4) (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [TensorProduct.CompatibleSMul R A M N] : TensorProduct A M N →ₗ[R] TensorProduct R M N
• LinearMap.lTensor_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) (n : N) : (LinearMap.lTensor M f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n
• LinearMap.rTensor_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) (n : N) : (LinearMap.rTensor M f) (n ⊗ₜ[R] m) = f n ⊗ₜ[R] m
• LinearMap.lTensor_comp_rTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : LinearMap.lTensor P g ∘ₗ LinearMap.rTensor N f = TensorProduct.map f g
• LinearMap.rTensor_comp_lTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : LinearMap.rTensor Q f ∘ₗ LinearMap.lTensor M g = TensorProduct.map f g
• TensorProduct.mapOfCompatibleSMul_surjective 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (A : Type u_4) (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [TensorProduct.CompatibleSMul R A M N] : Function.Surjective ⇑(TensorProduct.mapOfCompatibleSMul R A M N)
• TensorProduct.mapOfCompatibleSMul_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (A : Type u_4) (M : Type u_5) (N : Type u_6) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [CommSemiring A] [Module A M] [Module A N] [SMulCommClass R A M] [TensorProduct.CompatibleSMul R A M N] (m : M) (n : N) : (TensorProduct.mapOfCompatibleSMul R A M N) (m ⊗ₜ[A] n) = m ⊗ₜ[R] n
• LinearMap.lTensor_comp 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) : LinearMap.lTensor M (g ∘ₗ f) = LinearMap.lTensor M g ∘ₗ LinearMap.lTensor M f
• LinearMap.rTensor_comp 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) : LinearMap.rTensor M (g ∘ₗ f) = LinearMap.rTensor M g ∘ₗ LinearMap.rTensor M f
• TensorProduct.toLinearMap_congr 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : ↑(TensorProduct.congr f g) = TensorProduct.map ↑f ↑g
• TensorProduct.map_one 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : TensorProduct.map 1 1 = 1
• TensorProduct.mapIncl 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {P : Type u_7} {Q : Type u_8} [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] (p : Submodule R P) (q : Submodule R Q) : TensorProduct R ↥p ↥q →ₗ[R] TensorProduct R P Q
• LinearMap.lTensor_zero 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : LinearMap.lTensor M 0 = 0
• LinearMap.rTensor_zero 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : LinearMap.rTensor M 0 = 0
• TensorProduct.map_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (m : M) (n : N) : (TensorProduct.map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
• TensorProduct.liftAux.smul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N →ₗ[R] P} (r : R) (x : TensorProduct R M N) : (TensorProduct.liftAux f) (r • x) = r • (TensorProduct.liftAux f) x
• LinearEquiv.coe_lTensor_symm 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : ↑(LinearEquiv.lTensor M f).symm = LinearMap.lTensor M ↑f.symm
• LinearEquiv.coe_rTensor_symm 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N ≃ₗ[R] P) : ↑(LinearEquiv.rTensor M f).symm = LinearMap.rTensor M ↑f.symm
• TensorProduct.ext' 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {g h : TensorProduct R M N →ₗ[R] P} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)) : g = h
• LinearMap.lTensor_comp_map 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : LinearMap.lTensor P g' ∘ₗ TensorProduct.map f g = TensorProduct.map f (g' ∘ₗ g)
• LinearMap.map_comp_lTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) : TensorProduct.map f g ∘ₗ LinearMap.lTensor M g' = TensorProduct.map f (g ∘ₗ g')
• LinearMap.map_comp_rTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) : TensorProduct.map f g ∘ₗ LinearMap.rTensor N f' = TensorProduct.map (f ∘ₗ f') g
• LinearMap.rTensor_comp_map 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : LinearMap.rTensor Q f' ∘ₗ TensorProduct.map f g = TensorProduct.map (f' ∘ₗ f) g
• LinearMap.lTensor_neg 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : LinearMap.lTensor M (-f) = -LinearMap.lTensor M f
• LinearMap.rTensor_neg 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : LinearMap.rTensor M (-f) = -LinearMap.rTensor M f
• TensorProduct.map_zero_left 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : N →ₗ[R] Q) : TensorProduct.map 0 g = 0
• TensorProduct.map_zero_right 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) : TensorProduct.map f 0 = 0
• LinearMap.lTensorHom 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : (N →ₗ[R] P) →ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R M P
• LinearMap.rTensorHom 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : (N →ₗ[R] P) →ₗ[R] TensorProduct R N M →ₗ[R] TensorProduct R P M
• LinearMap.lTensor_bij_iff_rTensor_bij 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : Function.Bijective ⇑(LinearMap.lTensor M f) ↔ Function.Bijective ⇑(LinearMap.rTensor M f)
• LinearMap.lTensor_inj_iff_rTensor_inj 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : Function.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑(LinearMap.rTensor M f)
• LinearMap.lTensor_surj_iff_rTensor_surj 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Surjective ⇑(LinearMap.rTensor M f)
• TensorProduct.lift_compr₂ 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] {f : M →ₗ[R] N →ₗ[R] P} (g : P →ₗ[R] Q) : TensorProduct.lift (f.compr₂ g) = g ∘ₗ TensorProduct.lift f
• TensorProduct.lift_mk_compr₂ 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) : TensorProduct.lift ((TensorProduct.mk R M N).compr₂ f) = f
• TensorProduct.lift_comp_comm_eq 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) : TensorProduct.lift f ∘ₗ ↑(TensorProduct.comm R N M) = TensorProduct.lift f.flip
• LinearMap.lTensor_mul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : Module.End R N) : LinearMap.lTensor M (f * g) = LinearMap.lTensor M f * LinearMap.lTensor M g
• LinearMap.rTensor_mul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : Module.End R N) : LinearMap.rTensor M (f * g) = LinearMap.rTensor M f * LinearMap.rTensor M g
• TensorProduct.map_comp 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} {N₃ : Type u_16} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid N₁] [Module R N₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] [AddCommMonoid M₃] [Module R M₃] [AddCommMonoid N₃] [Module R N₃] (f₂ : M₂ →ₗ[R] M₃) (g₂ : N₂ →ₗ[R] N₃) (f₁ : M₁ →ₗ[R] M₂) (g₁ : N₁ →ₗ[R] N₂) : TensorProduct.map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) = TensorProduct.map f₂ g₂ ∘ₗ TensorProduct.map f₁ g₁
• TensorProduct.curry_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) (m : M) (n : N) : ((TensorProduct.curry f) m) n = f (m ⊗ₜ[R] n)
• TensorProduct.mapIncl.eq_1 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {P : Type u_7} {Q : Type u_8} [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] (p : Submodule R P) (q : Submodule R Q) : TensorProduct.mapIncl p q = TensorProduct.map p.subtype q.subtype
• TensorProduct.liftAux_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) : (TensorProduct.liftAux f) (m ⊗ₜ[R] n) = (f m) n
• LinearMap.lTensor_pow 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : N →ₗ[R] N) (n : ℕ) : LinearMap.lTensor M f ^ n = LinearMap.lTensor M (f ^ n)
• LinearMap.rTensor_pow 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] M) (n : ℕ) : LinearMap.rTensor N f ^ n = LinearMap.rTensor N (f ^ n)
• TensorProduct.lTensorHomToHomLTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (M : Type u_5) (P : Type u_7) (Q : Type u_8) [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R Q] [Module R P] : TensorProduct R P (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] TensorProduct R P Q
• TensorProduct.rTensorHomToHomRTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (M : Type u_5) (P : Type u_7) (Q : Type u_8) [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R Q] [Module R P] : TensorProduct R (M →ₗ[R] P) Q →ₗ[R] M →ₗ[R] TensorProduct R P Q
• TensorProduct.lift.tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N →ₗ[R] P} (x : M) (y : N) : (TensorProduct.lift f) (x ⊗ₜ[R] y) = (f x) y
• TensorProduct.map_range_eq_span_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : LinearMap.range (TensorProduct.map f g) = Submodule.span R {t | ∃ m n, f m ⊗ₜ[R] g n = t}
• LinearMap.comm_comp_lTensor_comp_comm_eq 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R Q] [Module R P] (g : N →ₗ[R] P) : ↑(TensorProduct.comm R Q P) ∘ₗ LinearMap.lTensor Q g ∘ₗ ↑(TensorProduct.comm R N Q) = LinearMap.rTensor Q g
• LinearMap.comm_comp_rTensor_comp_comm_eq 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R N] [Module R Q] [Module R P] (g : N →ₗ[R] P) : ↑(TensorProduct.comm R P Q) ∘ₗ LinearMap.rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N) = LinearMap.lTensor Q g
• TensorProduct.map₂ 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] (f : M →ₗ[R] P →ₗ[R] Q) (g : N →ₗ[R] S →ₗ[R] T) : TensorProduct R M N →ₗ[R] TensorProduct R P S →ₗ[R] TensorProduct R Q T
• TensorProduct.map_comp_comm_eq 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : TensorProduct.map f g ∘ₗ ↑(TensorProduct.comm R N M) = ↑(TensorProduct.comm R Q P) ∘ₗ TensorProduct.map g f
• LinearMap.lTensor_add 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f g : N →ₗ[R] P) : LinearMap.lTensor M (f + g) = LinearMap.lTensor M f + LinearMap.lTensor M g
• LinearMap.rTensor_add 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f g : N →ₗ[R] P) : LinearMap.rTensor M (f + g) = LinearMap.rTensor M f + LinearMap.rTensor M g
• TensorProduct.lift.tmul' 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N →ₗ[R] P} (x : M) (y : N) : (TensorProduct.lift f).toAddHom (x ⊗ₜ[R] y) = (f x) y
• TensorProduct.lift_comp_map 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] {Q' : Type u_18} [AddCommMonoid Q'] [Module R Q'] (i : P →ₗ[R] Q →ₗ[R] Q') (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : TensorProduct.lift i ∘ₗ TensorProduct.map f g = TensorProduct.lift ((i ∘ₗ f).compl₂ g)
• LinearMap.lTensor_smul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (r : R) (f : N →ₗ[R] P) : LinearMap.lTensor M (r • f) = r • LinearMap.lTensor M f
• LinearMap.rTensor_smul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (r : R) (f : N →ₗ[R] P) : LinearMap.rTensor M (r • f) = r • LinearMap.rTensor M f
• TensorProduct.lift.unique 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N →ₗ[R] P} {g : TensorProduct R M N →ₗ[R] P} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = (f x) y) : g = TensorProduct.lift f
• TensorProduct.map_pow 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] M) (g : N →ₗ[R] N) (n : ℕ) : TensorProduct.map f g ^ n = TensorProduct.map (f ^ n) (g ^ n)
• TensorProduct.map_add_left 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f₁ f₂ : M →ₗ[R] P) (g : N →ₗ[R] Q) : TensorProduct.map (f₁ + f₂) g = TensorProduct.map f₁ g + TensorProduct.map f₂ g
• TensorProduct.map_add_right 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g₁ g₂ : N →ₗ[R] Q) : TensorProduct.map f (g₁ + g₂) = TensorProduct.map f g₁ + TensorProduct.map f g₂
• TensorProduct.mk_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (m : M) (n : N) : ((TensorProduct.mk R M N) m) n = m ⊗ₜ[R] n
• TensorProduct.map_smul_left 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : TensorProduct.map (r • f) g = r • TensorProduct.map f g
• TensorProduct.map_smul_right 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (r : R) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : TensorProduct.map f (r • g) = r • TensorProduct.map f g
• LinearMap.lTensor_comp_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) (x : TensorProduct R M N) : (LinearMap.lTensor M (g ∘ₗ f)) x = (LinearMap.lTensor M g) ((LinearMap.lTensor M f) x)
• LinearMap.rTensor_comp_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P →ₗ[R] Q) (f : N →ₗ[R] P) (x : TensorProduct R N M) : (LinearMap.rTensor M (g ∘ₗ f)) x = (LinearMap.rTensor M g) ((LinearMap.rTensor M f) x)
• LinearMap.smul_lTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) {S : Type u_11} [CommSemiring S] [SMul R S] [Module S M] [IsScalarTower R S M] [SMulCommClass R S M] (s : S) (m : TensorProduct R M N) : s • (LinearMap.lTensor M f) m = (LinearMap.lTensor M f) (s • m)
• TensorProduct.map_mul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f₁ f₂ : M →ₗ[R] M) (g₁ g₂ : N →ₗ[R] N) : TensorProduct.map (f₁ * f₂) (g₁ * g₂) = TensorProduct.map f₁ g₁ * TensorProduct.map f₂ g₂
• TensorProduct.lcurry 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : (TensorProduct R M N →ₗ[R] P) →ₗ[R] M →ₗ[R] N →ₗ[R] P
• TensorProduct.uncurry 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : (M →ₗ[R] N →ₗ[R] P) →ₗ[R] TensorProduct R M N →ₗ[R] P
• TensorProduct.lift.equiv 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : (M →ₗ[R] N →ₗ[R] P) ≃ₗ[R] TensorProduct R M N →ₗ[R] P
• LinearMap.lTensor_sub 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f g : N →ₗ[R] P) : LinearMap.lTensor M (f - g) = LinearMap.lTensor M f - LinearMap.lTensor M g
• LinearMap.rTensor_sub 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (f g : N →ₗ[R] P) : LinearMap.rTensor M (f - g) = LinearMap.rTensor M f - LinearMap.rTensor M g
• TensorProduct.map_map 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14} {N₂ : Type u_15} {N₃ : Type u_16} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid N₁] [Module R N₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] [AddCommMonoid M₃] [Module R M₃] [AddCommMonoid N₃] [Module R N₃] (f₂ : M₂ →ₗ[R] M₃) (g₂ : N₂ →ₗ[R] N₃) (f₁ : M₁ →ₗ[R] M₂) (g₁ : N₁ →ₗ[R] N₂) (x : TensorProduct R M₁ N₁) : (TensorProduct.map f₂ g₂) ((TensorProduct.map f₁ g₁) x) = (TensorProduct.map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁)) x
• TensorProduct.homTensorHomMap 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) (Q : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] : TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q) →ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R P Q
• TensorProduct.ext 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {g h : TensorProduct R M N →ₗ[R] P} (H : (TensorProduct.mk R M N).compr₂ g = (TensorProduct.mk R M N).compr₂ h) : g = h
• TensorProduct.ext_iff 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] {g h : TensorProduct R M N →ₗ[R] P} : g = h ↔ (TensorProduct.mk R M N).compr₂ g = (TensorProduct.mk R M N).compr₂ h
• LinearMap.coe_lTensorHom 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : ⇑(LinearMap.lTensorHom M) = LinearMap.lTensor M
• LinearMap.coe_rTensorHom 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] : ⇑(LinearMap.rTensorHom M) = LinearMap.rTensor M
• TensorProduct.ext_threefold 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] {g h : TensorProduct R (TensorProduct R M N) P →ₗ[R] Q} (H : ∀ (x : M) (y : N) (z : P), g (x ⊗ₜ[R] y ⊗ₜ[R] z) = h (x ⊗ₜ[R] y ⊗ₜ[R] z)) : g = h
• TensorProduct.ext_threefold' 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] {g h : TensorProduct R M (TensorProduct R N P) →ₗ[R] Q} (H : ∀ (x : M) (y : N) (z : P), g (x ⊗ₜ[R] (y ⊗ₜ[R] z)) = h (x ⊗ₜ[R] (y ⊗ₜ[R] z))) : g = h
• TensorProduct.map_comm 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : TensorProduct R N M) : (TensorProduct.map f g) ((TensorProduct.comm R N M) x) = (TensorProduct.comm R Q P) ((TensorProduct.map g f) x)
• LinearMap.lTensor_comp_mk 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) : LinearMap.lTensor M f ∘ₗ (TensorProduct.mk R M N) m = (TensorProduct.mk R M P) m ∘ₗ f
• TensorProduct.range_mapIncl 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {P : Type u_7} {Q : Type u_8} [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] (p : Submodule R P) (q : Submodule R Q) : LinearMap.range (TensorProduct.mapIncl p q) = Submodule.span R (Set.image2 (fun x1 x2 => x1 ⊗ₜ[R] x2) ↑p ↑q)
• TensorProduct.lTensorHomToHomLTensor_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R Q] [Module R P] (p : P) (f : M →ₗ[R] Q) (m : M) : ((TensorProduct.lTensorHomToHomLTensor R M P Q) (p ⊗ₜ[R] f)) m = p ⊗ₜ[R] f m
• TensorProduct.rTensorHomToHomRTensor_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R Q] [Module R P] (f : M →ₗ[R] P) (q : Q) (m : M) : ((TensorProduct.rTensorHomToHomRTensor R M P Q) (f ⊗ₜ[R] q)) m = f m ⊗ₜ[R] q
• TensorProduct.map₂_apply_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] (f : M →ₗ[R] P →ₗ[R] Q) (g : N →ₗ[R] S →ₗ[R] T) (m : M) (n : N) : (TensorProduct.map₂ f g) (m ⊗ₜ[R] n) = TensorProduct.map (f m) (g n)
• TensorProduct.ext_fourfold' 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] {φ ψ : TensorProduct R (TensorProduct R M N) (TensorProduct R P Q) →ₗ[R] S} (H : ∀ (w : M) (x : N) (y : P) (z : Q), φ (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z)) = ψ (w ⊗ₜ[R] x ⊗ₜ[R] (y ⊗ₜ[R] z))) : φ = ψ
• TensorProduct.mapBilinear 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) (Q : Type u_8) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] : (M →ₗ[R] P) →ₗ[R] (N →ₗ[R] Q) →ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R P Q
• TensorProduct.map₂_eq_range_lift_comp_mapIncl 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R Q] [Module R P] (f : P →ₗ[R] Q →ₗ[R] M) (p : Submodule R P) (q : Submodule R Q) : Submodule.map₂ f p q = LinearMap.range (TensorProduct.lift f ∘ₗ TensorProduct.mapIncl p q)
• TensorProduct.lcurry_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) (m : M) (n : N) : (((TensorProduct.lcurry R M N P) f) m) n = f (m ⊗ₜ[R] n)
• TensorProduct.uncurry_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) : ((TensorProduct.uncurry R M N P) f) (m ⊗ₜ[R] n) = (f m) n
• TensorProduct.homTensorHomMap_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : (TensorProduct.homTensorHomMap R M N P Q) (f ⊗ₜ[R] g) = TensorProduct.map f g
• LinearMap.rTensor_comp_flip_mk 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) (m : M) : LinearMap.rTensor M f ∘ₗ (TensorProduct.mk R N M).flip m = (TensorProduct.mk R P M).flip m ∘ₗ f
• TensorProduct.ext_fourfold 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R P] {g h : TensorProduct R (TensorProduct R (TensorProduct R M N) P) Q →ₗ[R] S} (H : ∀ (w : M) (x : N) (y : P) (z : Q), g (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z) = h (w ⊗ₜ[R] x ⊗ₜ[R] y ⊗ₜ[R] z)) : g = h
• TensorProduct.lift.equiv_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) : ((TensorProduct.lift.equiv R M N P) f) (m ⊗ₜ[R] n) = (f m) n
• TensorProduct.range_mapIncl_mono 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {P : Type u_7} {Q : Type u_8} [AddCommMonoid P] [AddCommMonoid Q] [Module R Q] [Module R P] {p p' : Submodule R P} {q q' : Submodule R Q} (hp : p ≤ p') (hq : q ≤ q') : LinearMap.range (TensorProduct.mapIncl p q) ≤ LinearMap.range (TensorProduct.mapIncl p' q')
• TensorProduct.lift.equiv_symm_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  (R : Type u_1) [CommSemiring R] (M : Type u_5) (N : Type u_6) (P : Type u_7) [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : TensorProduct R M N →ₗ[R] P) (m : M) (n : N) : (((TensorProduct.lift.equiv R M N P).symm f) m) n = f (m ⊗ₜ[R] n)
• TensorProduct.mapBilinear_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : ((TensorProduct.mapBilinear R M N P Q) f) g = TensorProduct.map f g
• LinearMap.mul' 📋 Mathlib.Algebra.Algebra.Bilinear
  (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] : TensorProduct R A A →ₗ[R] A
• LinearMap.mul'_apply 📋 Mathlib.Algebra.Algebra.Bilinear
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] {a b : A} : (LinearMap.mul' R A) (a ⊗ₜ[R] b) = a * b
• LinearMap.lid_comp_rTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Associator
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : N →ₗ[R] R) : ↑(TensorProduct.lid R M) ∘ₗ LinearMap.rTensor M f = TensorProduct.lift (LinearMap.lsmul R M ∘ₗ f)
• LinearMap.rid_comp_lTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Associator
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] R) : ↑(TensorProduct.rid R N) ∘ₗ LinearMap.lTensor N f = TensorProduct.lift ((LinearMap.lsmul R N).flip.compl₂ f)
• TensorProduct.includeRight_lid 📋 Mathlib.LinearAlgebra.TensorProduct.Associator
  {R : Type u_1} [CommSemiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] {S : Type u_11} [Semiring S] [Algebra R S] (m : TensorProduct R R M) : 1 ⊗ₜ[R] (TensorProduct.lid R M) m = (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap) m
• LinearMap.lTensor_rTensor_comp_assoc 📋 Mathlib.LinearAlgebra.TensorProduct.Associator
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (x : M →ₗ[R] N) : LinearMap.lTensor P (LinearMap.rTensor Q x) ∘ₗ ↑(TensorProduct.assoc R P M Q) = ↑(TensorProduct.assoc R P N Q) ∘ₗ LinearMap.rTensor Q (LinearMap.lTensor P x)
• TensorProduct.map_map_comp_assoc_eq 📋 Mathlib.LinearAlgebra.TensorProduct.Associator
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) : TensorProduct.map f (TensorProduct.map g h) ∘ₗ ↑(TensorProduct.assoc R M N P) = ↑(TensorProduct.assoc R Q S T) ∘ₗ TensorProduct.map (TensorProduct.map f g) h
• LinearMap.lTensor_tensor 📋 Mathlib.LinearAlgebra.TensorProduct.Associator
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (f : P →ₗ[R] Q) : LinearMap.lTensor (TensorProduct R M N) f = ↑(TensorProduct.assoc R M N Q).symm ∘ₗ LinearMap.lTensor M (LinearMap.lTensor N f) ∘ₗ ↑(TensorProduct.assoc R M N P)
• LinearMap.rTensor_tensor 📋 Mathlib.LinearAlgebra.TensorProduct.Associator
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (g : P →ₗ[R] Q) : LinearMap.rTensor (TensorProduct R M N) g = ↑(TensorProduct.assoc R Q M N) ∘ₗ LinearMap.rTensor N (LinearMap.rTensor M g) ∘ₗ ↑(TensorProduct.assoc R P M N).symm
• LinearMap.rTensor_lTensor_comp_assoc_symm 📋 Mathlib.LinearAlgebra.TensorProduct.Associator
  {R : Type u_1} [CommSemiring R] (M : Type u_5) {N : Type u_6} {P : Type u_7} {Q : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R Q] [Module R P] (x : M →ₗ[R] N) : LinearMap.rTensor Q (LinearMap.lTensor P x) ∘ₗ ↑(TensorProduct.assoc R P M Q).symm = ↑(TensorProduct.assoc R P N Q).symm ∘ₗ LinearMap.lTensor P (LinearMap.rTensor Q x)
• TensorProduct.map_map_comp_assoc_symm_eq 📋 Mathlib.LinearAlgebra.TensorProduct.Associator
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) : TensorProduct.map (TensorProduct.map f g) h ∘ₗ ↑(TensorProduct.assoc R M N P).symm = ↑(TensorProduct.assoc R Q S T).symm ∘ₗ TensorProduct.map f (TensorProduct.map g h)
• TensorProduct.tensorTensorTensorComm_comp_map 📋 Mathlib.LinearAlgebra.TensorProduct.Associator
  (R : Type u_1) [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] {V : Type u_13} {W : Type u_14} [AddCommMonoid V] [AddCommMonoid W] [Module R V] [Module R W] (f : M →ₗ[R] S) (g : N →ₗ[R] T) (h : P →ₗ[R] V) (j : Q →ₗ[R] W) : ↑(TensorProduct.tensorTensorTensorComm R S T V W) ∘ₗ TensorProduct.map (TensorProduct.map f g) (TensorProduct.map h j) = TensorProduct.map (TensorProduct.map f h) (TensorProduct.map g j) ∘ₗ ↑(TensorProduct.tensorTensorTensorComm R M N P Q)
• TensorProduct.map_map_assoc 📋 Mathlib.LinearAlgebra.TensorProduct.Associator
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : TensorProduct R (TensorProduct R M N) P) : (TensorProduct.map f (TensorProduct.map g h)) ((TensorProduct.assoc R M N P) x) = (TensorProduct.assoc R Q S T) ((TensorProduct.map (TensorProduct.map f g) h) x)
• TensorProduct.map_map_assoc_symm 📋 Mathlib.LinearAlgebra.TensorProduct.Associator
  {R : Type u_1} [CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9} {T : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [AddCommMonoid T] [Module R M] [Module R N] [Module R Q] [Module R S] [Module R T] [Module R P] (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : TensorProduct R M (TensorProduct R N P)) : (TensorProduct.map (TensorProduct.map f g) h) ((TensorProduct.assoc R M N P).symm x) = (TensorProduct.assoc R Q S T).symm ((TensorProduct.map f (TensorProduct.map g h)) x)
• LinearMap.baseChange 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} (A : Type u_2) {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) : TensorProduct R A M →ₗ[A] TensorProduct R A N
• LinearMap.baseChange_id 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] : LinearMap.baseChange A LinearMap.id = LinearMap.id
• TensorProduct.AlgebraTensorModule.map_id 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] : TensorProduct.AlgebraTensorModule.map LinearMap.id LinearMap.id = LinearMap.id
• TensorProduct.AlgebraTensorModule.mk 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type uR) [CommSemiring R] (A : Type u_1) (M : Type u_2) (N : Type u_3) [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] [SMulCommClass R A M] [AddCommMonoid N] [Module R N] : M →ₗ[A] N →ₗ[R] TensorProduct R M N
• TensorProduct.AlgebraTensorModule.map 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : TensorProduct R M N →ₗ[A] TensorProduct R P Q
• TensorProduct.AlgebraTensorModule.map_eq 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map f g = TensorProduct.map f g
• TensorProduct.AlgebraTensorModule.curry 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : TensorProduct R M N →ₗ[A] P) : M →ₗ[A] N →ₗ[R] P
• TensorProduct.AlgebraTensorModule.lift 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M →ₗ[A] N →ₗ[R] P) : TensorProduct R M N →ₗ[A] P
• TensorProduct.AlgebraTensorModule.curry_injective 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] : Function.Injective TensorProduct.AlgebraTensorModule.curry
• TensorProduct.AlgebraTensorModule.curry_injective_iff 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] {a₁ a₂ : TensorProduct R M N →ₗ[A] P} : a₁ = a₂ ↔ TensorProduct.AlgebraTensorModule.curry a₁ = TensorProduct.AlgebraTensorModule.curry a₂
• LinearMap.baseChange_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) (a : A) (x : M) : (LinearMap.baseChange A f) (a ⊗ₜ[R] x) = a ⊗ₜ[R] f x
• TensorProduct.AlgebraTensorModule.map_one 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] : TensorProduct.AlgebraTensorModule.map 1 1 = 1
• LinearMap.baseChange_comp 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} {P : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) : LinearMap.baseChange A (g ∘ₗ f) = LinearMap.baseChange A g ∘ₗ LinearMap.baseChange A f
• LinearMap.baseChange_one 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type u_1) {A : Type u_2} (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] : LinearMap.baseChange A 1 = 1
• TensorProduct.AlgebraTensorModule.lTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} (A : Type uA) (M : Type uM) {N : Type uN} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] : (N →ₗ[R] Q) →ₗ[R] TensorProduct R M N →ₗ[A] TensorProduct R M Q
• TensorProduct.AlgebraTensorModule.map_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) (m : M) (n : N) : (TensorProduct.AlgebraTensorModule.map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
• TensorProduct.AlgebraTensorModule.rTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type uR) {A : Type uA} {M : Type uM} (N : Type uN) {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] : (M →ₗ[A] P) →ₗ[R] TensorProduct R M N →ₗ[A] TensorProduct R P N
• TensorProduct.AlgebraTensorModule.ext 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] {g h : TensorProduct R M N →ₗ[A] P} (H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = h (x ⊗ₜ[R] y)) : g = h
• TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] (a : A) (x : TensorProduct R M N) : a • x = (LinearMap.rTensor N ((Algebra.lsmul R R M) a)) x
• LinearMap.baseChange_zero 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : LinearMap.baseChange A 0 = 0
• TensorProduct.AlgebraTensorModule.lift_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M →ₗ[A] N →ₗ[R] P) (x : M) (y : N) : (TensorProduct.AlgebraTensorModule.lift f) (x ⊗ₜ[R] y) = (f x) y
• LinearMap.baseChangeHom 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : (M →ₗ[R] N) →ₗ[R] TensorProduct R A M →ₗ[A] TensorProduct R A N
• TensorProduct.AlgebraTensorModule.mk_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type uR) [CommSemiring R] (A : Type u_1) (M : Type u_2) (N : Type u_3) [Semiring A] [AddCommMonoid M] [Module R M] [Module A M] [SMulCommClass R A M] [AddCommMonoid N] [Module R N] (m : M) : (TensorProduct.AlgebraTensorModule.mk R A M N) m = { toFun := fun x2 => m ⊗ₜ[R] x2, map_add' := ⋯, map_smul' := ⋯ }
• LinearMap.baseChange_eq_ltensor 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) : ⇑(LinearMap.baseChange A f) = ⇑(LinearMap.lTensor A f)
• TensorProduct.AlgebraTensorModule.map_comp 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} {P' : Type uP'} {Q' : Type uQ'} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [AddCommMonoid P'] [Module R P'] [Module A P'] [IsScalarTower R A P'] [AddCommMonoid Q'] [Module R Q'] (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) = TensorProduct.AlgebraTensorModule.map f₂ g₂ ∘ₗ TensorProduct.AlgebraTensorModule.map f₁ g₁
• TensorProduct.AlgebraTensorModule.curry_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : TensorProduct R M N →ₗ[A] P) (a : M) : (TensorProduct.AlgebraTensorModule.curry f) a = (TensorProduct.curry (↑R f)) a
• LinearMap.baseChange_neg 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : LinearMap.baseChange A (-f) = -LinearMap.baseChange A f
• LinearMap.baseChange_pow 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type u_1) (A : Type u_2) (M : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : Module.End R M) (n : ℕ) : LinearMap.baseChange A (f ^ n) = LinearMap.baseChange A f ^ n
• TensorProduct.AlgebraTensorModule.map_mul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] (f₁ f₂ : M →ₗ[A] M) (g₁ g₂ : N →ₗ[R] N) : TensorProduct.AlgebraTensorModule.map (f₁ * f₂) (g₁ * g₂) = TensorProduct.AlgebraTensorModule.map f₁ g₁ * TensorProduct.AlgebraTensorModule.map f₂ g₂
• TensorProduct.AlgebraTensorModule.lcurry 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] : (TensorProduct R M N →ₗ[A] P) →ₗ[B] M →ₗ[A] N →ₗ[R] P
• TensorProduct.AlgebraTensorModule.uncurry 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] : (M →ₗ[A] N →ₗ[R] P) →ₗ[B] TensorProduct R M N →ₗ[A] P
• LinearMap.baseChange_mul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f g : Module.End R M) : LinearMap.baseChange A (f * g) = LinearMap.baseChange A f * LinearMap.baseChange A g
• TensorProduct.AlgebraTensorModule.lift.equiv 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] : (M →ₗ[A] N →ₗ[R] P) ≃ₗ[B] TensorProduct R M N →ₗ[A] P
• TensorProduct.AlgebraTensorModule.map_add_left 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map (f₁ + f₂) g = TensorProduct.AlgebraTensorModule.map f₁ g + TensorProduct.AlgebraTensorModule.map f₂ g
• TensorProduct.AlgebraTensorModule.map_smul_right 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (r : R) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map f (r • g) = r • TensorProduct.AlgebraTensorModule.map f g
• TensorProduct.AlgebraTensorModule.map_add_right 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g₁ g₂ : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map f (g₁ + g₂) = TensorProduct.AlgebraTensorModule.map f g₁ + TensorProduct.AlgebraTensorModule.map f g₂
• Submodule.baseChange.eq_1 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule.baseChange A p = LinearMap.range (LinearMap.baseChange A p.subtype)
• LinearMap.baseChange_smul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (r : R) (f : M →ₗ[R] N) : LinearMap.baseChange A (r • f) = r • LinearMap.baseChange A f
• TensorProduct.AlgebraTensorModule.map_smul_left 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (b : B) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map (b • f) g = b • TensorProduct.AlgebraTensorModule.map f g
• LinearMap.baseChange_add 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f g : M →ₗ[R] N) : LinearMap.baseChange A (f + g) = LinearMap.baseChange A f + LinearMap.baseChange A g
• TensorProduct.AlgebraTensorModule.rTensor_id 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] : (TensorProduct.AlgebraTensorModule.rTensor R N) LinearMap.id = LinearMap.id
• TensorProduct.AlgebraTensorModule.homTensorHomMap 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] : TensorProduct R (M →ₗ[A] P) (N →ₗ[R] Q) →ₗ[B] TensorProduct R M N →ₗ[A] TensorProduct R P Q
• TensorProduct.AlgebraTensorModule.lTensor_id 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] : (TensorProduct.AlgebraTensorModule.lTensor A M) LinearMap.id = LinearMap.id
• TensorProduct.AlgebraTensorModule.lift_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M →ₗ[A] N →ₗ[R] P) (a : TensorProduct R M N) : (TensorProduct.AlgebraTensorModule.lift f) a = (TensorProduct.lift (↑R f)) a
• Submodule.baseChange_span 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (s : Set M) : Submodule.baseChange A (Submodule.span R s) = Submodule.span A (⇑((TensorProduct.mk R A M) 1) '' s)
• TensorProduct.AlgebraTensorModule.rTensor_one 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] : (TensorProduct.AlgebraTensorModule.rTensor R N) 1 = 1
• TensorProduct.AlgebraTensorModule.rTensor_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M →ₗ[A] P) (m : M) (n : N) : ((TensorProduct.AlgebraTensorModule.rTensor R N) f) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] n
• TensorProduct.AlgebraTensorModule.lTensor_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] (f : N →ₗ[R] Q) (m : M) (n : N) : ((TensorProduct.AlgebraTensorModule.lTensor A M) f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n
• TensorProduct.AlgebraTensorModule.restrictScalars_curry 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : TensorProduct R M N →ₗ[A] P) : ↑R (TensorProduct.AlgebraTensorModule.curry f) = TensorProduct.curry (↑R f)
• TensorProduct.AlgebraTensorModule.lTensor_one 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] : (TensorProduct.AlgebraTensorModule.lTensor A M) 1 = 1
• LinearMap.rTensor_baseChange 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (φ : A →ₐ[R] B) (t : TensorProduct R A M) (f : M →ₗ[R] N) : (LinearMap.rTensor N φ.toLinearMap) ((LinearMap.baseChange A f) t) = (LinearMap.baseChange B f) ((LinearMap.rTensor M φ.toLinearMap) t)
• TensorProduct.AlgebraTensorModule.coe_lTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] (f : N →ₗ[R] Q) : ⇑((TensorProduct.AlgebraTensorModule.lTensor A M) f) = ⇑(LinearMap.lTensor M f)
• Submodule.baseChange_eq_span 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {M : Type u_2} (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Submodule.baseChange A p = Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) p)
• LinearMap.baseChange_sub 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type u_1} {A : Type u_2} {M : Type u_4} {N : Type u_5} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f g : M →ₗ[R] N) : LinearMap.baseChange A (f - g) = LinearMap.baseChange A f - LinearMap.baseChange A g
• TensorProduct.AlgebraTensorModule.coe_rTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M →ₗ[A] P) : ⇑((TensorProduct.AlgebraTensorModule.rTensor R N) f) = ⇑(LinearMap.rTensor N (↑R f))
• LinearMap.baseChangeHom_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) : (LinearMap.baseChangeHom R A M N) f = LinearMap.baseChange A f
• TensorProduct.AlgebraTensorModule.lcurry_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : TensorProduct R M N →ₗ[A] P) : (TensorProduct.AlgebraTensorModule.lcurry R A B M N P) f = TensorProduct.AlgebraTensorModule.curry f
• TensorProduct.AlgebraTensorModule.uncurry_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : M →ₗ[A] N →ₗ[R] P) : (TensorProduct.AlgebraTensorModule.uncurry R A B M N P) f = TensorProduct.AlgebraTensorModule.lift f
• TensorProduct.AlgebraTensorModule.restrictScalars_lTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid Q] [Module R Q] (f : N →ₗ[R] Q) : ↑R ((TensorProduct.AlgebraTensorModule.lTensor A M) f) = LinearMap.lTensor M f
• TensorProduct.AlgebraTensorModule.restrictScalars_rTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] (f : M →ₗ[A] P) : ↑R ((TensorProduct.AlgebraTensorModule.rTensor R N) f) = LinearMap.rTensor N (↑R f)
• TensorProduct.AlgebraTensorModule.mapBilinear 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type uR) (A : Type uA) (B : Type uB) (M : Type uM) (N : Type uN) (P : Type uP) (Q : Type uQ) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] : (M →ₗ[A] P) →ₗ[B] (N →ₗ[R] Q) →ₗ[R] TensorProduct R M N →ₗ[A] TensorProduct R P Q
• TensorProduct.AlgebraTensorModule.homTensorHomMap_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : (TensorProduct.AlgebraTensorModule.homTensorHomMap R A B M N P Q) (f ⊗ₜ[R] g) = TensorProduct.AlgebraTensorModule.map f g
• TensorProduct.AlgebraTensorModule.rTensor_comp 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {P' : Type uP'} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid P'] [Module R P'] [Module A P'] [IsScalarTower R A P'] (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P) : (TensorProduct.AlgebraTensorModule.rTensor R N) (f₂ ∘ₗ f₁) = (TensorProduct.AlgebraTensorModule.rTensor R N) f₂ ∘ₗ (TensorProduct.AlgebraTensorModule.rTensor R N) f₁

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision ff04530 serving mathlib revision fe81dd4