Loogle!

Result

Found 138 declarations mentioning TensorProduct.map.

• TensorProduct.map 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : TensorProduct R M N →ₛₗ[σ₁₂] TensorProduct R₂ M₂ N₂
• TensorProduct.map_id 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_7) {N : Type u_8} {P : Type u_9} [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_comp_rTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : LinearMap.rTensor Q f ∘ₗ LinearMap.lTensor M g = TensorProduct.map f g
• TensorProduct.toLinearMap_congr 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) : ↑(TensorProduct.congr f g) = TensorProduct.map ↑f ↑g
• TensorProduct.map_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) (m : M) (n : N) : (TensorProduct.map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R₂] g n
• TensorProduct.map_one 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : TensorProduct.map 1 1 = 1
• TensorProduct.map_bijective 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] {f : M →ₗ[R] N} {g : P →ₗ[R] Q} (hf : Function.Bijective ⇑f) (hg : Function.Bijective ⇑g) : Function.Bijective ⇑(TensorProduct.map f g)
• TensorProduct.map_zero_left 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (g : N →ₛₗ[σ₁₂] N₂) : TensorProduct.map 0 g = 0
• TensorProduct.map_zero_right 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) : TensorProduct.map f 0 = 0
• LinearMap.lTensor_comp_map 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (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_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (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
• TensorProduct.map_comp 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f₂ : M₂ →ₛₗ[σ₂₃] M₃) (g₂ : N₂ →ₛₗ[σ₂₃] N₃) (f₁ : M →ₛₗ[σ₁₂] M₂) (g₁ : N →ₛₗ[σ₁₂] N₂) : TensorProduct.map (f₂ ∘ₛₗ f₁) (g₂ ∘ₛₗ g₁) = TensorProduct.map f₂ g₂ ∘ₛₗ TensorProduct.map f₁ g₁
• TensorProduct.mapIncl.eq_1 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {P : Type u_9} {Q : Type u_10} [AddCommMonoid P] [AddCommMonoid Q] [Module R P] [Module R Q] (p : Submodule R P) (q : Submodule R Q) : TensorProduct.mapIncl p q = TensorProduct.map p.subtype q.subtype
• TensorProduct.lift_comp_map 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} {P₃ : Type u_18} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid P₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ P₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (i : M₂ →ₛₗ[σ₂₃] N₂ →ₛₗ[σ₂₃] P₃) (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : TensorProduct.lift i ∘ₛₗ TensorProduct.map f g = TensorProduct.lift ((i ∘ₛₗ f).compl₂ g)
• TensorProduct.map_range_eq_span_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (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}
• TensorProduct.range_map_eq_span_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (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}
• TensorProduct.map_comp_comm_eq 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : TensorProduct.map f g ∘ₛₗ ↑(TensorProduct.comm R N M) = ↑(TensorProduct.comm R₂ N₂ M₂) ∘ₛₗ TensorProduct.map g f
• TensorProduct.map_add_left 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f₁ f₂ : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : 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} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g₁ g₂ : N →ₛₗ[σ₁₂] N₂) : TensorProduct.map f (g₁ + g₂) = TensorProduct.map f g₁ + TensorProduct.map f g₂
• TensorProduct.map_smul_left 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (r : R₂) (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : TensorProduct.map (r • f) g = r • TensorProduct.map f g
• TensorProduct.map_smul_right 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (r : R₂) (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : TensorProduct.map f (r • g) = r • TensorProduct.map f g
• TensorProduct.range_map 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) : LinearMap.range (TensorProduct.map f g) = Submodule.map₂ (TensorProduct.mk R P Q) (LinearMap.range f) (LinearMap.range g)
• TensorProduct.map_pow 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [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)
• LinearMap.lTensor_map 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (g' : Q →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : TensorProduct R M N) : (LinearMap.lTensor P g') ((TensorProduct.map f g) x) = (TensorProduct.map f (g' ∘ₗ g)) x
• LinearMap.map_lTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) (x : TensorProduct R M S) : (TensorProduct.map f g) ((LinearMap.lTensor M g') x) = (TensorProduct.map f (g ∘ₗ g')) x
• LinearMap.map_rTensor 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) (x : TensorProduct R S N) : (TensorProduct.map f g) ((LinearMap.rTensor N f') x) = (TensorProduct.map (f ∘ₗ f') g) x
• LinearMap.rTensor_map 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [AddCommMonoid S] [Module R M] [Module R N] [Module R S] [Module R P] [Module R Q] (f' : P →ₗ[R] S) (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : TensorProduct R M N) : (LinearMap.rTensor Q f') ((TensorProduct.map f g) x) = (TensorProduct.map (f' ∘ₗ f) g) x
• TensorProduct.map_mul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [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.map_map 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f₂ : M₂ →ₛₗ[σ₂₃] M₃) (g₂ : N₂ →ₛₗ[σ₂₃] N₃) (f₁ : M →ₛₗ[σ₁₂] M₂) (g₁ : N →ₛₗ[σ₁₂] N₂) (x : TensorProduct R M N) : (TensorProduct.map f₂ g₂) ((TensorProduct.map f₁ g₁) x) = (TensorProduct.map (f₂ ∘ₛₗ f₁) (g₂ ∘ₛₗ g₁)) x
• TensorProduct.map_comm 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) (x : TensorProduct R N M) : (TensorProduct.map f g) ((TensorProduct.comm R N M) x) = (TensorProduct.comm R₂ N₂ M₂) ((TensorProduct.map g f) x)
• TensorProduct.range_map_mono 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R M₂] [Module R M₃] [Module R N₂] [Module R N₃] {a : M →ₗ[R] M₂} {b : M₃ →ₗ[R] M₂} {c : N →ₗ[R] N₂} {d : N₃ →ₗ[R] N₂} (hab : LinearMap.range a ≤ LinearMap.range b) (hcd : LinearMap.range c ≤ LinearMap.range d) : LinearMap.range (TensorProduct.map a c) ≤ LinearMap.range (TensorProduct.map b d)
• TensorProduct.map₂_apply_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [CommSemiring R] [CommSemiring R₂] [CommSemiring R₃] {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid M₃] [AddCommMonoid N₃] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] [Module R₃ M₃] [Module R₃ N₃] (f : M →ₛₗ[σ₁₃] M₂ →ₛₗ[σ₂₃] M₃) (g : N →ₛₗ[σ₁₃] N₂ →ₛₗ[σ₂₃] N₃) (m : M) (n : N) : (TensorProduct.map₂ f g) (m ⊗ₜ[R] n) = TensorProduct.map (f m) (g n)
• TensorProduct.homTensorHomMap_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : (TensorProduct.homTensorHomMap σ₁₂ M N M₂ N₂) (f ⊗ₜ[R₂] g) = TensorProduct.map f g
• TensorProduct.mapBilinear_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basic
  {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g : N →ₛₗ[σ₁₂] N₂) : ((TensorProduct.mapBilinear σ₁₂ M N M₂ N₂) f) g = TensorProduct.map f g
• AlgHom.comp_mul' 📋 Mathlib.Algebra.Algebra.Bilinear
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : f.toLinearMap ∘ₗ LinearMap.mul' R A = LinearMap.mul' R B ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap
• NonUnitalAlgHom.comp_mul' 📋 Mathlib.Algebra.Algebra.Bilinear
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] (f : A →ₙₐ[R] B) : ↑f ∘ₗ LinearMap.mul' R A = LinearMap.mul' R B ∘ₗ TensorProduct.map ↑f ↑f
• 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
• 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)
• 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
• LinearMap.mulLeft_tmul 📋 Mathlib.RingTheory.TensorProduct.Basic
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] (a : A) (b : B) : LinearMap.mulLeft R (a ⊗ₜ[R] b) = TensorProduct.map (LinearMap.mulLeft R a) (LinearMap.mulLeft R b)
• LinearMap.mulRight_tmul 📋 Mathlib.RingTheory.TensorProduct.Basic
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] (a : A) (b : B) : LinearMap.mulRight R (a ⊗ₜ[R] b) = TensorProduct.map (LinearMap.mulRight R a) (LinearMap.mulRight R b)
• TensorProduct.Algebra.linearMap_comp_mul' 📋 Mathlib.RingTheory.TensorProduct.Basic
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] : Algebra.linearMap R (TensorProduct R A B) ∘ₗ LinearMap.mul' R R = TensorProduct.map (Algebra.linearMap R A) (Algebra.linearMap R B)
• TensorProduct.Algebra.mul'_comp_tensorTensorTensorComm 📋 Mathlib.RingTheory.TensorProduct.Basic
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] : LinearMap.mul' R (TensorProduct R A B) ∘ₗ ↑(TensorProduct.tensorTensorTensorComm R A A B B) = TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R B)
• LinearMap.mul'_tensor 📋 Mathlib.RingTheory.TensorProduct.Basic
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B] : LinearMap.mul' R (TensorProduct R A B) = TensorProduct.map (LinearMap.mul' R A) (LinearMap.mul' R B) ∘ₗ ↑(TensorProduct.tensorTensorTensorComm R A B A B)
• TensorProduct.map_surjective 📋 Mathlib.LinearAlgebra.TensorProduct.RightExactness
  {R : Type u_1} [CommSemiring R] {N : Type u_3} {P : Type u_4} [AddCommMonoid N] [AddCommMonoid P] [Module R N] [Module R P] {g : N →ₗ[R] P} (hg : Function.Surjective ⇑g) {N' : Type u_6} {P' : Type u_7} [AddCommMonoid N'] [AddCommMonoid P'] [Module R N'] [Module R P'] {g' : N' →ₗ[R] P'} (hg' : Function.Surjective ⇑g') : Function.Surjective ⇑(TensorProduct.map g g')
• TensorProduct.map_ker 📋 Mathlib.LinearAlgebra.TensorProduct.RightExactness
  {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) {M' : Type u_6} {N' : Type u_7} {P' : Type u_8} [AddCommGroup M'] [AddCommGroup N'] [AddCommGroup P'] [Module R M'] [Module R N'] [Module R P'] {f' : M' →ₗ[R] N'} {g' : N' →ₗ[R] P'} (hfg' : Function.Exact ⇑f' ⇑g') (hg' : Function.Surjective ⇑g') : LinearMap.ker (TensorProduct.map g g') = LinearMap.range (LinearMap.lTensor N f') ⊔ LinearMap.range (LinearMap.rTensor N' f)
• IsTensorProduct.map.eq_1 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N] [Module R N₁] [Module R N₂] [Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) : hf.map hg i₁ i₂ = ↑hg.equiv ∘ₗ TensorProduct.map i₁ i₂ ∘ₗ ↑hf.equiv.symm
• TensorProduct.exists_finite_submodule_of_finite' 📋 Mathlib.LinearAlgebra.TensorProduct.Finiteness
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {M₁ : Submodule R M} {N₁ : Submodule R N} (s : Set (TensorProduct R ↥M₁ ↥N₁)) (hs : s.Finite) : ∃ M' N', ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁), Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (TensorProduct.map (Submodule.inclusion hM) (Submodule.inclusion hN)))
• TensorProduct.exists_finite_submodule_of_setFinite' 📋 Mathlib.LinearAlgebra.TensorProduct.Finiteness
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {M₁ : Submodule R M} {N₁ : Submodule R N} (s : Set (TensorProduct R ↥M₁ ↥N₁)) (hs : s.Finite) : ∃ M' N', ∃ (hM : M' ≤ M₁) (hN : N' ≤ N₁), Module.Finite R ↥M' ∧ Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (TensorProduct.map (Submodule.inclusion hM) (Submodule.inclusion hN)))
• TensorProduct.map_injective_of_flat_flat 📋 Mathlib.RingTheory.Flat.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {P : Type u_4} {Q : Type u_5} [AddCommMonoid P] [Module R P] [AddCommMonoid Q] [Module R Q] (f : P →ₗ[R] M) (g : Q →ₗ[R] N) [Module.Flat R M] [Module.Flat R Q] (hf : Function.Injective ⇑f) (hg : Function.Injective ⇑g) : Function.Injective ⇑(TensorProduct.map f g)
• TensorProduct.map_injective_of_flat_flat' 📋 Mathlib.RingTheory.Flat.Basic
  {R : Type u_1} [CommSemiring R] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {P : Type u_4} {Q : Type u_5} [AddCommMonoid P] [Module R P] [AddCommMonoid Q] [Module R Q] (f : P →ₗ[R] M) (g : Q →ₗ[R] N) [Module.Flat R P] [Module.Flat R N] (hf : Function.Injective ⇑f) (hg : Function.Injective ⇑g) : Function.Injective ⇑(TensorProduct.map f g)
• SemimoduleCat.hom_tensorHom 📋 Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
  {R : Type u} [CommSemiring R] {K L M N : SemimoduleCat R} (f : K ⟶ L) (g : M ⟶ N) : SemimoduleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = TensorProduct.map (SemimoduleCat.Hom.hom f) (SemimoduleCat.Hom.hom g)
• SemimoduleCat.MonoidalCategory.tensorHom.eq_1 📋 Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
  {R : Type u} [CommSemiring R] {M N : SemimoduleCat R} {M' N' : SemimoduleCat R} (f : M ⟶ N) (g : M' ⟶ N') : SemimoduleCat.MonoidalCategory.tensorHom f g = SemimoduleCat.ofHom (TensorProduct.map (SemimoduleCat.Hom.hom f) (SemimoduleCat.Hom.hom g))
• ModuleCat.hom_tensorHom 📋 Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
  {R : Type u} [CommRing R] {K L M N : ModuleCat R} (f : K ⟶ L) (g : M ⟶ N) : ModuleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) = TensorProduct.map (ModuleCat.Hom.hom f) (ModuleCat.Hom.hom g)
• ModuleCat.MonoidalCategory.tensorHom_def 📋 Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
  {R : Type u} [CommRing R] {X₁✝ Y₁✝ X₂✝ Y₂✝ : ModuleCat R} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = ModuleCat.ofHom (TensorProduct.map (ModuleCat.Hom.hom f) (ModuleCat.Hom.hom g))
• Prod.comul_comp_fst 📋 Mathlib.RingTheory.Coalgebra.Basic
  (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.comul ∘ₗ LinearMap.fst R A B = TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ CoalgebraStruct.comul
• Prod.comul_comp_snd 📋 Mathlib.RingTheory.Coalgebra.Basic
  (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.comul ∘ₗ LinearMap.snd R A B = TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ CoalgebraStruct.comul
• Finsupp.comul_comp_lapply 📋 Mathlib.RingTheory.Coalgebra.Basic
  (R : Type u) (ι : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (i : ι) : CoalgebraStruct.comul ∘ₗ Finsupp.lapply i = TensorProduct.map (Finsupp.lapply i) (Finsupp.lapply i) ∘ₗ CoalgebraStruct.comul
• Prod.comul_comp_inl 📋 Mathlib.RingTheory.Coalgebra.Basic
  (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.comul ∘ₗ LinearMap.inl R A B = TensorProduct.map (LinearMap.inl R A B) (LinearMap.inl R A B) ∘ₗ CoalgebraStruct.comul
• Prod.comul_comp_inr 📋 Mathlib.RingTheory.Coalgebra.Basic
  (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] : CoalgebraStruct.comul ∘ₗ LinearMap.inr R A B = TensorProduct.map (LinearMap.inr R A B) (LinearMap.inr R A B) ∘ₗ CoalgebraStruct.comul
• DFinsupp.comul_comp_lapply 📋 Mathlib.RingTheory.Coalgebra.Basic
  (R : Type u) (ι : Type v) (A : ι → Type w) [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [(i : ι) → Coalgebra R (A i)] (i : ι) : CoalgebraStruct.comul ∘ₗ DFinsupp.lapply i = TensorProduct.map (DFinsupp.lapply i) (DFinsupp.lapply i) ∘ₗ CoalgebraStruct.comul
• Finsupp.comul_comp_lsingle 📋 Mathlib.RingTheory.Coalgebra.Basic
  (R : Type u) (ι : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (i : ι) : CoalgebraStruct.comul ∘ₗ Finsupp.lsingle i = TensorProduct.map (Finsupp.lsingle i) (Finsupp.lsingle i) ∘ₗ CoalgebraStruct.comul
• DFinsupp.comul_comp_lsingle 📋 Mathlib.RingTheory.Coalgebra.Basic
  (R : Type u) (ι : Type v) (A : ι → Type w) [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [(i : ι) → Coalgebra R (A i)] (i : ι) : CoalgebraStruct.comul ∘ₗ DFinsupp.lsingle i = TensorProduct.map (DFinsupp.lsingle i) (DFinsupp.lsingle i) ∘ₗ CoalgebraStruct.comul
• Finsupp.comul_single 📋 Mathlib.RingTheory.Coalgebra.Basic
  (R : Type u) (ι : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] (i : ι) (a : A) : (CoalgebraStruct.comul fun₀ | i => a) = (TensorProduct.map (Finsupp.lsingle i) (Finsupp.lsingle i)) (CoalgebraStruct.comul a)
• DFinsupp.comul_single 📋 Mathlib.RingTheory.Coalgebra.Basic
  (R : Type u) (ι : Type v) (A : ι → Type w) [DecidableEq ι] [CommSemiring R] [(i : ι) → AddCommMonoid (A i)] [(i : ι) → Module R (A i)] [(i : ι) → Coalgebra R (A i)] (i : ι) (a : A i) : (CoalgebraStruct.comul fun₀ | i => a) = (TensorProduct.map (DFinsupp.lsingle i) (DFinsupp.lsingle i)) (CoalgebraStruct.comul a)
• Prod.comul_apply 📋 Mathlib.RingTheory.Coalgebra.Basic
  (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] (r : A × B) : CoalgebraStruct.comul r = (TensorProduct.map (LinearMap.inl R A B) (LinearMap.inl R A B)) (CoalgebraStruct.comul r.1) + (TensorProduct.map (LinearMap.inr R A B) (LinearMap.inr R A B)) (CoalgebraStruct.comul r.2)
• CoalgHom.map_comp_comul 📋 Mathlib.RingTheory.Coalgebra.Hom
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (self : A →ₗc[R] B) : TensorProduct.map self.toLinearMap self.toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ self.toLinearMap
• CoalgHomClass.map_comp_comul 📋 Mathlib.RingTheory.Coalgebra.Hom
  {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst✝ : CommSemiring R} {inst✝¹ : AddCommMonoid A} {inst✝² : Module R A} {inst✝³ : AddCommMonoid B} {inst✝⁴ : Module R B} {inst✝⁵ : CoalgebraStruct R A} {inst✝⁶ : CoalgebraStruct R B} {inst✝⁷ : FunLike F A B} [self : CoalgHomClass F R A B] (f : F) : TensorProduct.map ↑f ↑f ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ ↑f
• CoalgHom.mk 📋 Mathlib.RingTheory.Coalgebra.Hom
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (toLinearMap : A →ₗ[R] B) (counit_comp : CoalgebraStruct.counit ∘ₗ toLinearMap = CoalgebraStruct.counit) (map_comp_comul : TensorProduct.map toLinearMap toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ toLinearMap) : A →ₗc[R] B
• CoalgHom.coe_mk 📋 Mathlib.RingTheory.Coalgebra.Hom
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A →ₗ[R] B} (h : CoalgebraStruct.counit ∘ₗ f = CoalgebraStruct.counit) (h₁ : TensorProduct.map f f ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ f) : ⇑{ toLinearMap := f, counit_comp := h, map_comp_comul := h₁ } = ⇑f
• CoalgHomClass.map_comp_comul_apply 📋 Mathlib.RingTheory.Coalgebra.Hom
  {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [FunLike F A B] [CoalgHomClass F R A B] (f : F) (x : A) : (TensorProduct.map ↑f ↑f) (CoalgebraStruct.comul x) = CoalgebraStruct.comul (f x)
• CoalgHomClass.mk 📋 Mathlib.RingTheory.Coalgebra.Hom
  {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [FunLike F A B] [toSemilinearMapClass : SemilinearMapClass F (RingHom.id R) A B] (counit_comp : ∀ (f : F), CoalgebraStruct.counit ∘ₗ ↑f = CoalgebraStruct.counit) (map_comp_comul : ∀ (f : F), TensorProduct.map ↑f ↑f ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ ↑f) : CoalgHomClass F R A B
• CoalgHom.coe_linearMap_mk 📋 Mathlib.RingTheory.Coalgebra.Hom
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A →ₗ[R] B} (h : CoalgebraStruct.counit ∘ₗ f = CoalgebraStruct.counit) (h₁ : TensorProduct.map f f ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ f) : ↑{ toLinearMap := f, counit_comp := h, map_comp_comul := h₁ } = f
• CoalgHom.coe_mks 📋 Mathlib.RingTheory.Coalgebra.Hom
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A → B} (h₁ : ∀ (x y : A), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : A), { toFun := f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h₁ }.toFun x) (h₃ : CoalgebraStruct.counit ∘ₗ { toFun := f, map_add' := h₁, map_smul' := h₂ } = CoalgebraStruct.counit) (h₄ : TensorProduct.map { toFun := f, map_add' := h₁, map_smul' := h₂ } { toFun := f, map_add' := h₁, map_smul' := h₂ } ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ { toFun := f, map_add' := h₁, map_smul' := h₂ }) : ⇑{ toFun := f, map_add' := h₁, map_smul' := h₂, counit_comp := h₃, map_comp_comul := h₄ } = f
• CoalgHom.mk.injEq 📋 Mathlib.RingTheory.Coalgebra.Hom
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (toLinearMap : A →ₗ[R] B) (counit_comp : CoalgebraStruct.counit ∘ₗ toLinearMap = CoalgebraStruct.counit) (map_comp_comul : TensorProduct.map toLinearMap toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ toLinearMap) (toLinearMap✝ : A →ₗ[R] B) (counit_comp✝ : CoalgebraStruct.counit ∘ₗ toLinearMap✝ = CoalgebraStruct.counit) (map_comp_comul✝ : TensorProduct.map toLinearMap✝ toLinearMap✝ ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ toLinearMap✝) : ({ toLinearMap := toLinearMap, counit_comp := counit_comp, map_comp_comul := map_comp_comul } = { toLinearMap := toLinearMap✝, counit_comp := counit_comp✝, map_comp_comul := map_comp_comul✝ }) = (toLinearMap = toLinearMap✝)
• CoalgHom.mk_coe 📋 Mathlib.RingTheory.Coalgebra.Hom
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A →ₗc[R] B} (h₁ : ∀ (x y : A), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : A), { toFun := ⇑f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₁ }.toFun x) (h₃ : CoalgebraStruct.counit ∘ₗ { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ } = CoalgebraStruct.counit) (h₄ : TensorProduct.map { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ } { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ } ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }) : { toFun := ⇑f, map_add' := h₁, map_smul' := h₂, counit_comp := h₃, map_comp_comul := h₄ } = f
• CoalgHom.mk.sizeOf_spec 📋 Mathlib.RingTheory.Coalgebra.Hom
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] [SizeOf R] [SizeOf A] [SizeOf B] (toLinearMap : A →ₗ[R] B) (counit_comp : CoalgebraStruct.counit ∘ₗ toLinearMap = CoalgebraStruct.counit) (map_comp_comul : TensorProduct.map toLinearMap toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ toLinearMap) : sizeOf { toLinearMap := toLinearMap, counit_comp := counit_comp, map_comp_comul := map_comp_comul } = 1 + sizeOf toLinearMap + sizeOf counit_comp + sizeOf map_comp_comul
• TensorProduct.congr.eq_1 📋 Mathlib.RingTheory.Coalgebra.Equiv
  {R : Type u_1} {R₂ : Type u_2} [CommSemiring R] [CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7} {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid M₂] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R₂ M₂] [Module R₂ N₂] {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : M ≃ₛₗ[σ₁₂] M₂) (g : N ≃ₛₗ[σ₁₂] N₂) : TensorProduct.congr f g = LinearEquiv.ofLinear (TensorProduct.map ↑f ↑g) (TensorProduct.map ↑f.symm ↑g.symm) ⋯ ⋯
• CoalgEquiv.coe_mk 📋 Mathlib.RingTheory.Coalgebra.Equiv
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A → B} {h : ∀ (x y : A), f (x + y) = f x + f y} {h₀ : ∀ (m : R) (x : A), { toFun := f, map_add' := h }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h }.toFun x} {h₁ : CoalgebraStruct.counit ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ } = CoalgebraStruct.counit} {h₂ : TensorProduct.map { toFun := f, map_add' := h, map_smul' := h₀ } { toFun := f, map_add' := h, map_smul' := h₀ } ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ { toFun := f, map_add' := h, map_smul' := h₀ }} {h₃ : B → A} {h₄ : Function.LeftInverse h₃ { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ }.toFun} {h₅ : Function.RightInverse h₃ { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂ }.toFun} : ⇑{ toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅ } = f
• BialgHom.coe_mks 📋 Mathlib.RingTheory.Bialgebra.Hom
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A → B} (h₀ : ∀ (x y : A), f (x + y) = f x + f y) (h₁ : ∀ (m : R) (x : A), { toFun := f, map_add' := h₀ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h₀ }.toFun x) (h₂ : CoalgebraStruct.counit ∘ₗ { toFun := f, map_add' := h₀, map_smul' := h₁ } = CoalgebraStruct.counit) (h₃ : TensorProduct.map { toFun := f, map_add' := h₀, map_smul' := h₁ } { toFun := f, map_add' := h₀, map_smul' := h₁ } ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ { toFun := f, map_add' := h₀, map_smul' := h₁ }) (h₄ : { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun 1 = 1) (h₅ : ∀ (x y : A), { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun (x * y) = { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun x * { toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun y) : ⇑{ toFun := f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃, map_one' := h₄, map_mul' := h₅ } = f
• BialgHom.mk_coe 📋 Mathlib.RingTheory.Bialgebra.Hom
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] {f : A →ₐc[R] B} (h₀ : ∀ (x y : A), f (x + y) = f x + f y) (h₁ : ∀ (m : R) (x : A), { toFun := ⇑f, map_add' := h₀ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₀ }.toFun x) (h₂ : CoalgebraStruct.counit ∘ₗ { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ } = CoalgebraStruct.counit) (h₃ : TensorProduct.map { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ } { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ } ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ { toFun := ⇑f, map_add' := h₀, map_smul' := h₁ }) (h₄ : { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun 1 = 1) (h₅ : ∀ (x y : A), { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun (x * y) = { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun x * { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃ }.toFun y) : { toFun := ⇑f, map_add' := h₀, map_smul' := h₁, counit_comp := h₂, map_comp_comul := h₃, map_one' := h₄, map_mul' := h₅ } = f
• CoalgCat.MonoidalCategoryAux.tensorHom_toLinearMap 📋 Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
  {R : Type u} [CommRing R] {M N P Q : Type u} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Coalgebra R M] [Coalgebra R N] [Coalgebra R P] [Coalgebra R Q] (f : M →ₗc[R] N) (g : P →ₗc[R] Q) : (CategoryTheory.MonoidalCategoryStruct.tensorHom (CoalgCat.ofHom f) (CoalgCat.ofHom g)).toCoalgHom'.toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap
• CoalgCat.MonoidalCategoryAux.tensorObj_comul 📋 Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
  {R : Type u} [CommRing R] (K L : CoalgCat R) : CoalgebraStruct.comul = ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul
• IsLocalization.instIsLocalizedModuleTensorProductMap 📋 Mathlib.RingTheory.Localization.BaseChange
  {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_3} [AddCommMonoid M] [Module R M] {M' : Type u_4} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (N : Type u_5) (N' : Type u_6) [AddCommMonoid N] [Module R N] [AddCommMonoid N'] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S f] [IsLocalizedModule S g] : IsLocalizedModule S (TensorProduct.map f g)
• map_dualTensorHom 📋 Mathlib.LinearAlgebra.Contraction
  {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : Module.Dual R M) (p : P) (g : Module.Dual R N) (q : Q) : TensorProduct.map ((dualTensorHom R M P) (f ⊗ₜ[R] p)) ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) = (dualTensorHom R (TensorProduct R M N) (TensorProduct R P Q)) ((TensorProduct.dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] (p ⊗ₜ[R] q))
• TensorProduct.quotientTensorEquiv 📋 Mathlib.LinearAlgebra.TensorProduct.Quotient
  {R : Type u_1} {M : Type u_2} (N : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : Submodule R M) : TensorProduct R (M ⧸ m) N ≃ₗ[R] TensorProduct R M N ⧸ LinearMap.range (TensorProduct.map m.subtype LinearMap.id)
• TensorProduct.tensorQuotientEquiv 📋 Mathlib.LinearAlgebra.TensorProduct.Quotient
  {R : Type u_1} (M : Type u_2) {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (n : Submodule R N) : TensorProduct R M (N ⧸ n) ≃ₗ[R] TensorProduct R M N ⧸ LinearMap.range (TensorProduct.map LinearMap.id n.subtype)
• TensorProduct.quotientTensorQuotientEquiv 📋 Mathlib.LinearAlgebra.TensorProduct.Quotient
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : Submodule R M) (n : Submodule R N) : TensorProduct R (M ⧸ m) (N ⧸ n) ≃ₗ[R] TensorProduct R M N ⧸ LinearMap.range (TensorProduct.map m.subtype LinearMap.id) ⊔ LinearMap.range (TensorProduct.map LinearMap.id n.subtype)
• TensorProduct.quotientTensorEquiv_apply_tmul_mk 📋 Mathlib.LinearAlgebra.TensorProduct.Quotient
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : Submodule R M) (x : M) (y : N) : (TensorProduct.quotientTensorEquiv N m) (Submodule.Quotient.mk x ⊗ₜ[R] y) = Submodule.Quotient.mk (x ⊗ₜ[R] y)
• TensorProduct.tensorQuotientEquiv_apply_mk_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Quotient
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (n : Submodule R N) (x : M) (y : N) : (TensorProduct.tensorQuotientEquiv M n) (x ⊗ₜ[R] Submodule.Quotient.mk y) = Submodule.Quotient.mk (x ⊗ₜ[R] y)
• TensorProduct.quotientTensorEquiv_symm_apply_mk_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Quotient
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : Submodule R M) (x : M) (y : N) : (TensorProduct.quotientTensorEquiv N m).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) = Submodule.Quotient.mk x ⊗ₜ[R] y
• TensorProduct.tensorQuotientEquiv_symm_apply_tmul_mk 📋 Mathlib.LinearAlgebra.TensorProduct.Quotient
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (n : Submodule R N) (x : M) (y : N) : (TensorProduct.tensorQuotientEquiv M n).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) = x ⊗ₜ[R] Submodule.Quotient.mk y
• TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk 📋 Mathlib.LinearAlgebra.TensorProduct.Quotient
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : Submodule R M) (n : Submodule R N) (x : M) (y : N) : (TensorProduct.quotientTensorQuotientEquiv m n) (Submodule.Quotient.mk x ⊗ₜ[R] Submodule.Quotient.mk y) = Submodule.Quotient.mk (x ⊗ₜ[R] y)
• TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Quotient
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : Submodule R M) (n : Submodule R N) (x : M) (y : N) : (TensorProduct.quotientTensorQuotientEquiv m n).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) = Submodule.Quotient.mk x ⊗ₜ[R] Submodule.Quotient.mk y
• LinearMap.trace_tensorProduct' 📋 Mathlib.LinearAlgebra.Trace
  {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] (f : M →ₗ[R] M) (g : N →ₗ[R] N) : (LinearMap.trace R (TensorProduct R M N)) (TensorProduct.map f g) = (LinearMap.trace R M) f * (LinearMap.trace R N) g
• TensorProduct.LieModule.toLinearMap_map 📋 Mathlib.Algebra.Lie.TensorProduct
  {R : Type u} [CommRing R] {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} {Q : Type w₃} [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [AddCommGroup P] [Module R P] [LieRingModule L P] [LieModule R L P] [AddCommGroup Q] [Module R Q] [LieRingModule L Q] [LieModule R L Q] (f : M →ₗ⁅R,L⁆ P) (g : N →ₗ⁅R,L⁆ Q) : ↑(TensorProduct.LieModule.map f g) = TensorProduct.map ↑f ↑g
• Representation.tprod_apply 📋 Mathlib.RepresentationTheory.Basic
  {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) (g : G) : (ρV.tprod ρW) g = TensorProduct.map (ρV g) (ρW g)
• Representation.dualTensorHom_comm 📋 Mathlib.RepresentationTheory.Basic
  {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) (g : G) : dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g) = (ρV.linHom ρW) g ∘ₗ dualTensorHom k V W
• TensorProduct.intrinsicStar_map 📋 Mathlib.Algebra.Star.LinearMap
  {R : Type u_5} {E : Type u_6} {F : Type u_7} {G : Type u_8} {H : Type u_9} [CommSemiring R] [StarRing R] [AddCommMonoid E] [StarAddMonoid E] [Module R E] [StarModule R E] [AddCommMonoid F] [StarAddMonoid F] [Module R F] [StarModule R F] [AddCommMonoid G] [StarAddMonoid G] [Module R G] [StarModule R G] [AddCommMonoid H] [StarAddMonoid H] [Module R H] [StarModule R H] (f : E →ₗ[R] F) (g : G →ₗ[R] H) : star (TensorProduct.map f g) = TensorProduct.map (star f) (star g)
• TensorProduct.norm_map 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H) (x : TensorProduct 𝕜 E F) : ‖(TensorProduct.map f.toLinearMap g.toLinearMap) x‖ = ‖x‖
• TensorProduct.toLinearMap_mapIsometry 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H) : (TensorProduct.mapIsometry f g).toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap
• TensorProduct.nnnorm_map 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H) (x : TensorProduct 𝕜 E F) : ‖(TensorProduct.map f.toLinearMap g.toLinearMap) x‖₊ = ‖x‖₊
• TensorProduct.inner_map_map 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H) (x y : TensorProduct 𝕜 E F) : inner 𝕜 ((TensorProduct.map f.toLinearMap g.toLinearMap) x) ((TensorProduct.map f.toLinearMap g.toLinearMap) y) = inner 𝕜 x y
• TensorProduct.enorm_map 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H) (x : TensorProduct 𝕜 E F) : ‖(TensorProduct.map f.toLinearMap g.toLinearMap) x‖ₑ = ‖x‖ₑ
• TensorProduct.mapIsometry_apply 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : E →ₗᵢ[𝕜] G) (g : F →ₗᵢ[𝕜] H) (x : TensorProduct 𝕜 E F) : (TensorProduct.mapIsometry f g) x = (TensorProduct.map f.toLinearMap g.toLinearMap) x
• TensorProduct.adjoint_map 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] [FiniteDimensional 𝕜 H] (f : E →ₗ[𝕜] F) (g : G →ₗ[𝕜] H) : LinearMap.adjoint (TensorProduct.map f g) = TensorProduct.map (LinearMap.adjoint f) (LinearMap.adjoint g)
• Submodule.mulMap_comp_map_inclusion 📋 Mathlib.LinearAlgebra.TensorProduct.Submodule
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {M N M' N' : Submodule R S} (hM : M' ≤ M) (hN : N' ≤ N) : M.mulMap N ∘ₗ TensorProduct.map (Submodule.inclusion hM) (Submodule.inclusion hN) = M'.mulMap N'
• Submodule.mulMap_map_comp_eq 📋 Mathlib.LinearAlgebra.TensorProduct.Submodule
  {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] (M N : Submodule R S) {T : Type w} [Semiring T] [Algebra R T] {F : Type u_1} [FunLike F S T] [AlgHomClass F R S T] (f : F) : (Submodule.map f M).mulMap (Submodule.map f N) ∘ₗ TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N) = ↑f ∘ₗ M.mulMap N
• Algebra.TensorProduct.linearEquivIncludeRange_toLinearMap 📋 Mathlib.LinearAlgebra.TensorProduct.Subalgebra
  (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [Semiring T] [Algebra R T] : ↑(Algebra.TensorProduct.linearEquivIncludeRange R S T) = TensorProduct.map Algebra.TensorProduct.includeLeft.toLinearMap.rangeRestrict Algebra.TensorProduct.includeRight.toLinearMap.rangeRestrict
• Algebra.TensorProduct.opAlgEquiv_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Opposite
  (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [IsScalarTower R S A] (x : TensorProduct R Aᵐᵒᵖ Bᵐᵒᵖ) : (Algebra.TensorProduct.opAlgEquiv R S A B) x = MulOpposite.op ((TensorProduct.map ↑(MulOpposite.opLinearEquiv R).symm ↑(MulOpposite.opLinearEquiv R).symm) x)
• Algebra.TensorProduct.opAlgEquiv_symm_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Opposite
  (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [IsScalarTower R S A] (x : (TensorProduct R A B)ᵐᵒᵖ) : (Algebra.TensorProduct.opAlgEquiv R S A B).symm x = (TensorProduct.map ↑(MulOpposite.opLinearEquiv R) ↑(MulOpposite.opLinearEquiv R)) (MulOpposite.unop x)
• CliffordAlgebra.toBaseChange_involute 📋 Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
  {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (x : CliffordAlgebra (QuadraticForm.baseChange A Q)) : (CliffordAlgebra.toBaseChange A Q) (CliffordAlgebra.involute x) = (TensorProduct.map LinearMap.id CliffordAlgebra.involute.toLinearMap) ((CliffordAlgebra.toBaseChange A Q) x)
• CliffordAlgebra.toBaseChange_reverse 📋 Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
  {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (x : CliffordAlgebra (QuadraticForm.baseChange A Q)) : (CliffordAlgebra.toBaseChange A Q) (CliffordAlgebra.reverse x) = (TensorProduct.map LinearMap.id CliffordAlgebra.reverse) ((CliffordAlgebra.toBaseChange A Q) x)
• TensorProduct.gradedMul_def 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
  (R : Type u_5) {ι : Type u_6} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_7) (ℬ : ι → Type u_8) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] [DirectSum.GRing 𝒜] [DirectSum.GRing ℬ] [DirectSum.GAlgebra R 𝒜] [DirectSum.GAlgebra R ℬ] : TensorProduct.gradedMul R 𝒜 ℬ = TensorProduct.curry (TensorProduct.map (LinearMap.mul' R (DirectSum ι fun i => 𝒜 i)) (LinearMap.mul' R (DirectSum ι fun i => ℬ i)) ∘ₗ ↑(TensorProduct.assoc R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => 𝒜 i) (TensorProduct R (DirectSum ι fun i => ℬ i) (DirectSum ι fun i => ℬ i))).symm ∘ₗ LinearMap.lTensor (DirectSum ι fun i => 𝒜 i) (↑(TensorProduct.assoc R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => ℬ i) (DirectSum ι fun i => ℬ i)) ∘ₗ LinearMap.rTensor (DirectSum ι fun i => ℬ i) ↑(TensorProduct.gradedComm R ℬ 𝒜) ∘ₗ ↑(TensorProduct.assoc R (DirectSum ι ℬ) (DirectSum ι 𝒜) (DirectSum ι ℬ)).symm) ∘ₗ ↑(TensorProduct.assoc R (DirectSum ι 𝒜) (DirectSum ι ℬ) (TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ))))
• QuadraticForm.tmul_comp_tensorMap 📋 Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
  {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} {M₄ : Type uM₄} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [AddCommGroup M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [Invertible 2] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄} (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) : QuadraticMap.comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃
• QuadraticForm.tmul_tensorMap_apply 📋 Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
  {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} {M₄ : Type uM₄} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [AddCommGroup M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [Invertible 2] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄} (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) (x : TensorProduct R M₁ M₃) : (Q₂.tmul Q₄) ((TensorProduct.map f.toLinearMap g.toLinearMap) x) = (Q₁.tmul Q₃) x
• QuadraticMap.Isometry.tmul_apply 📋 Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
  {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} {M₄ : Type uM₄} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [AddCommGroup M₄] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [Invertible 2] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄} (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) (x : TensorProduct R M₁ M₃) : (f.tmul g) x = (TensorProduct.map f.toLinearMap g.toLinearMap) x
• Matrix.toLin_kronecker 📋 Mathlib.LinearAlgebra.TensorProduct.Matrix
  {R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_5} {N' : Type u_6} {ι : Type u_7} {κ : Type u_8} {ι' : Type u_10} {κ' : Type u_11} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [Finite ι'] [Finite κ'] [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup M'] [AddCommGroup N'] [Module R M] [Module R N] [Module R M'] [Module R N'] (bM : Module.Basis ι R M) (bN : Module.Basis κ R N) (bM' : Module.Basis ι' R M') (bN' : Module.Basis κ' R N') (A : Matrix ι' ι R) (B : Matrix κ' κ R) : (Matrix.toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B) = TensorProduct.map ((Matrix.toLin bM bM') A) ((Matrix.toLin bN bN') B)
• TensorProduct.toMatrix_map 📋 Mathlib.LinearAlgebra.TensorProduct.Matrix
  {R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_5} {N' : Type u_6} {ι : Type u_7} {κ : Type u_8} {ι' : Type u_10} {κ' : Type u_11} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [Finite ι'] [Finite κ'] [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup M'] [AddCommGroup N'] [Module R M] [Module R N] [Module R M'] [Module R N'] (bM : Module.Basis ι R M) (bN : Module.Basis κ R N) (bM' : Module.Basis ι' R M') (bN' : Module.Basis κ' R N') (f : M →ₗ[R] M') (g : N →ₗ[R] N') : (LinearMap.toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN')) (TensorProduct.map f g) = Matrix.kroneckerMap (fun x1 x2 => x1 * x2) ((LinearMap.toMatrix bM bM') f) ((LinearMap.toMatrix bN bN') g)
• TensorProduct.map_injective_of_flat_flat_of_isDomain 📋 Mathlib.RingTheory.Flat.Domain
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : Type u_4} {Q : Type u_5} [AddCommGroup P] [Module R P] [AddCommGroup Q] [Module R Q] (f : P →ₗ[R] M) (g : Q →ₗ[R] N) [H : Module.Flat R P] [Module.Flat R Q] (hf : Function.Injective ⇑f) (hg : Function.Injective ⇑g) : Function.Injective ⇑(TensorProduct.map f g)
• AddMonoidAlgebra.comul_single 📋 Mathlib.RingTheory.Coalgebra.MonoidAlgebra
  {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] {X : Type u_3} [Module R A] [Coalgebra R A] (x : X) (a : A) : CoalgebraStruct.comul (AddMonoidAlgebra.single x a) = (TensorProduct.map (AddMonoidAlgebra.lsingle x) (AddMonoidAlgebra.lsingle x)) (CoalgebraStruct.comul a)
• MonoidAlgebra.comul_single 📋 Mathlib.RingTheory.Coalgebra.MonoidAlgebra
  {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] {X : Type u_3} [Module R A] [Coalgebra R A] (x : X) (a : A) : CoalgebraStruct.comul (MonoidAlgebra.single x a) = (TensorProduct.map (MonoidAlgebra.lsingle x) (MonoidAlgebra.lsingle x)) (CoalgebraStruct.comul a)
• LaurentPolynomial.comul_C 📋 Mathlib.RingTheory.Coalgebra.MonoidAlgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Module R A] [Coalgebra R A] (a : A) : CoalgebraStruct.comul (LaurentPolynomial.C a) = (TensorProduct.map (AddMonoidAlgebra.lsingle 0) (AddMonoidAlgebra.lsingle 0)) (CoalgebraStruct.comul a)
• LaurentPolynomial.comul_C_mul_T 📋 Mathlib.RingTheory.Coalgebra.MonoidAlgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Module R A] [Coalgebra R A] (a : A) (n : ℤ) : CoalgebraStruct.comul (LaurentPolynomial.C a * LaurentPolynomial.T n) = (TensorProduct.map (AddMonoidAlgebra.lsingle n) (AddMonoidAlgebra.lsingle n)) (CoalgebraStruct.comul a)
• LinearMap.convMul_def 📋 Mathlib.RingTheory.Coalgebra.Convolution
  {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] (f g : C →ₗ[R] A) : f * g = LinearMap.mul' R A ∘ₗ TensorProduct.map f g ∘ₗ CoalgebraStruct.comul
• LinearMap.convMul_apply 📋 Mathlib.RingTheory.Coalgebra.Convolution
  {R : Type u_1} {A : Type u_2} {C : Type u_4} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] (f g : C →ₗ[R] A) (c : C) : (f * g) c = (LinearMap.mul' R A) ((TensorProduct.map f g) (CoalgebraStruct.comul c))
• TensorProduct.map_convMul_map 📋 Mathlib.RingTheory.Coalgebra.Convolution
  {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [AddCommMonoid C] [Module R C] [CoalgebraStruct R C] {D : Type u_5} [AddCommMonoid B] [Module R B] [CoalgebraStruct R B] [NonUnitalNonAssocSemiring D] [Module R D] [SMulCommClass R D D] [IsScalarTower R D D] {f h : C →ₗ[R] A} {g k : B →ₗ[R] D} : TensorProduct.map f g * TensorProduct.map h k = TensorProduct.map (f * h) (g * k)
• MulOpposite.comul_def 📋 Mathlib.RingTheory.Coalgebra.MulOpposite
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [CoalgebraStruct R A] : CoalgebraStruct.comul = TensorProduct.map ↑(MulOpposite.opLinearEquiv R) ↑(MulOpposite.opLinearEquiv R) ∘ₗ CoalgebraStruct.comul ∘ₗ ↑(MulOpposite.opLinearEquiv R).symm

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 6ff4759 serving mathlib revision edaf32c