Loogle!

Result

Found 114 declarations mentioning TensorProduct.map.

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
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.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.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
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
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
TensorProduct.map_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] {P' : Type u_11} {Q' : Type u_12} [AddCommMonoid P'] [Module R P'] [AddCommMonoid Q'] [Module R Q'] (f₂ : P →ₗ[R] P') (f₁ : M →ₗ[R] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) : 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_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.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}
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
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_12} [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)
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.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
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.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)
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.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
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
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.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] [Semiring A] [Semiring B] [Algebra R A] [Algebra R 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)
ModuleCat.MonoidalCategory.instMonoidalCategoryStruct_tensorHom 📋 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))
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.counit_def 📋 Mathlib.RingTheory.Coalgebra.Basic
{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] : CoalgebraStruct.counit = LinearMap.mul' R R ∘ₗ TensorProduct.map CoalgebraStruct.counit CoalgebraStruct.counit
TensorProduct.instCoalgebraStruct_counit 📋 Mathlib.RingTheory.Coalgebra.Basic
{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] : CoalgebraStruct.counit = LinearMap.mul' R R ∘ₗ TensorProduct.map CoalgebraStruct.counit CoalgebraStruct.counit
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
TensorProduct.comul_def 📋 Mathlib.RingTheory.Coalgebra.Basic
{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] : CoalgebraStruct.comul = ↑(TensorProduct.tensorTensorTensorComm R A A B B) ∘ₗ TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul
TensorProduct.instCoalgebraStruct_comul 📋 Mathlib.RingTheory.Coalgebra.Basic
{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] : CoalgebraStruct.comul = ↑(TensorProduct.tensorTensorTensorComm R A A B B) ∘ₗ TensorProduct.map CoalgebraStruct.comul 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} [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 = 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.ofAlgHom 📋 Mathlib.RingTheory.Bialgebra.Hom
{R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐ[R] B) (counit_comp : CoalgebraStruct.counit ∘ₗ f.toLinearMap = CoalgebraStruct.counit) (map_comp_comul : TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ f.toLinearMap) : A →ₐc[R] B
BialgHom.ofAlgHom_apply 📋 Mathlib.RingTheory.Bialgebra.Hom
{R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [CoalgebraStruct R A] [CoalgebraStruct R B] (f : A →ₐ[R] B) (counit_comp : CoalgebraStruct.counit ∘ₗ f.toLinearMap = CoalgebraStruct.counit) (map_comp_comul : TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ f.toLinearMap) (a✝ : A) : (BialgHom.ofAlgHom f counit_comp map_comp_comul) a✝ = (↑↑f.toRingHom).toFun a✝
BialgHom.coe_mks 📋 Mathlib.RingTheory.Bialgebra.Hom
{R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [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] [Algebra R A] [Semiring B] [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
BialgEquiv.coe_mk 📋 Mathlib.RingTheory.Bialgebra.Equiv
{R : Type u} {A : Type v} {B : Type w} [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₃ : 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} {h₆ : ∀ (x y : A), { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅ }.toFun (x * y) = { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅ }.toFun x * { toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅ }.toFun y} : ⇑{ toFun := f, map_add' := h, map_smul' := h₀, counit_comp := h₁, map_comp_comul := h₂, invFun := h₃, left_inv := h₄, right_inv := h₅, map_mul' := h₆ } = f
CoalgebraCat.MonoidalCategoryAux.tensorHom_toLinearMap 📋 Mathlib.Algebra.Category.CoalgebraCat.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 (CoalgebraCat.ofHom f) (CoalgebraCat.ofHom g)).toCoalgHom'.toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap
CoalgebraCat.MonoidalCategoryAux.tensorObj_comul 📋 Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence
{R : Type u} [CommRing R] (K L : CoalgebraCat R) : CoalgebraStruct.comul = ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul
Coalgebra.TensorProduct.map_toLinearMap 📋 Mathlib.RingTheory.Coalgebra.TensorProduct
{R M N P Q : Type u} [CommRing R] [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) : ↑(Coalgebra.TensorProduct.map f g) = 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.antipode_def 📋 Mathlib.RingTheory.HopfAlgebra.TensorProduct
{R A B : Type u} [CommRing R] [Ring A] [Ring B] [HopfAlgebra R A] [HopfAlgebra R B] : HopfAlgebraStruct.antipode = TensorProduct.map HopfAlgebraStruct.antipode HopfAlgebraStruct.antipode
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)
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
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)
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.coe_linearMap_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
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
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 : Basis ι R M) (bN : Basis κ R N) (bM' : Basis ι' R M') (bN' : 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 : Basis ι R M) (bN : Basis κ R N) (bM' : Basis ι' R M') (bN' : 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)
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)
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)

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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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 19971e9 serving mathlib revision bce1d65