Loogle!

Result

Found 169 declarations mentioning TensorProduct and Prod.

• TensorProduct.SMul.aux 📋 Mathlib.LinearAlgebra.TensorProduct.Defs
  {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R' : Type u_22} [SMul R' M] (r : R') : FreeAddMonoid (M × N) →+ TensorProduct R M N
• TensorProduct.SMul.aux_of 📋 Mathlib.LinearAlgebra.TensorProduct.Defs
  {R : Type u_1} [CommSemiring R] {M : Type u_7} {N : Type u_8} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {R' : Type u_22} [SMul R' M] (r : R') (m : M) (n : N) : (TensorProduct.SMul.aux r) (FreeAddMonoid.of (m, n)) = (r • m) ⊗ₜ[R] n
• TensorProduct.directSum 📋 Mathlib.LinearAlgebra.DirectSum.TensorProduct
  (R : Type u) [CommSemiring R] (S : Type u_1) [Semiring S] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] (M₁ : ι₁ → Type w₁) (M₂ : ι₂ → Type w₂) [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] : TensorProduct R (DirectSum ι₁ fun i₁ => M₁ i₁) (DirectSum ι₂ fun i₂ => M₂ i₂) ≃ₗ[S] DirectSum (ι₁ × ι₂) fun i => TensorProduct R (M₁ i.1) (M₂ i.2)
• TensorProduct.directSum_lof_tmul_lof 📋 Mathlib.LinearAlgebra.DirectSum.TensorProduct
  (R : Type u) [CommSemiring R] (S : Type u_1) [Semiring S] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] {M₁ : ι₁ → Type w₁} {M₂ : ι₂ → Type w₂} [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) : (TensorProduct.directSum R S M₁ M₂) ((DirectSum.lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i₂) m₂) = (DirectSum.lof S (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)
• TensorProduct.directSum_symm_lof_tmul 📋 Mathlib.LinearAlgebra.DirectSum.TensorProduct
  (R : Type u) [CommSemiring R] (S : Type u_1) [Semiring S] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] {M₁ : ι₁ → Type w₁} {M₂ : ι₂ → Type w₂} [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] (i₁ : ι₁) (m₁ : M₁ i₁) (i₂ : ι₂) (m₂ : M₂ i₂) : (TensorProduct.directSum R S M₁ M₂).symm ((DirectSum.lof S (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) (m₁ ⊗ₜ[R] m₂)) = (DirectSum.lof S ι₁ M₁ i₁) m₁ ⊗ₜ[R] (DirectSum.lof R ι₂ M₂ i₂) m₂
• finsuppTensorFinsuppLid 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid N] [Module R N] : TensorProduct R (ι →₀ R) (κ →₀ N) ≃ₗ[R] ι × κ →₀ N
• finsuppTensorFinsuppRid 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorProduct R (ι →₀ M) (κ →₀ R) ≃ₗ[R] ι × κ →₀ M
• finsuppTensorFinsupp' 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] : TensorProduct R (ι →₀ R) (κ →₀ R) ≃ₗ[R] ι × κ →₀ R
• finsuppTensorFinsuppLid_self 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] : finsuppTensorFinsuppLid R R ι κ = finsuppTensorFinsupp' R ι κ
• finsuppTensorFinsuppRid_self 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] : finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ
• finsuppTensorFinsupp 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] : TensorProduct R (ι →₀ M) (κ →₀ N) ≃ₗ[S] ι × κ →₀ TensorProduct R M N
• finsuppTensorFinsuppLid_single_tmul_single 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid N] [Module R N] (a : ι) (b : κ) (r : R) (n : N) : (finsuppTensorFinsuppLid R N ι κ) ((fun₀ | a => r) ⊗ₜ[R] fun₀ | b => n) = fun₀ | (a, b) => r • n
• finsuppTensorFinsuppRid_single_tmul_single 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : ι) (b : κ) (m : M) (r : R) : (finsuppTensorFinsuppRid R M ι κ) ((fun₀ | a => m) ⊗ₜ[R] fun₀ | b => r) = fun₀ | (a, b) => r • m
• finsuppTensorFinsuppLid_apply_apply 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid N] [Module R N] (f : ι →₀ R) (g : κ →₀ N) (a : ι) (b : κ) : ((finsuppTensorFinsuppLid R N ι κ) (f ⊗ₜ[R] g)) (a, b) = f a • g b
• finsuppTensorFinsuppRid_apply_apply 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] (f : ι →₀ M) (g : κ →₀ R) (a : ι) (b : κ) : ((finsuppTensorFinsuppRid R M ι κ) (f ⊗ₜ[R] g)) (a, b) = g b • f a
• finsuppTensorFinsupp'_single_tmul_single 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] (a : ι) (b : κ) (r₁ r₂ : R) : (finsuppTensorFinsupp' R ι κ) ((fun₀ | a => r₁) ⊗ₜ[R] fun₀ | b => r₂) = fun₀ | (a, b) => r₁ * r₂
• finsuppTensorFinsupp'_apply_apply 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] (f : ι →₀ R) (g : κ →₀ R) (a : ι) (b : κ) : ((finsuppTensorFinsupp' R ι κ) (f ⊗ₜ[R] g)) (a, b) = f a * g b
• finsuppTensorFinsuppLid_symm_single_smul 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid N] [Module R N] (i : ι × κ) (r : R) (n : N) : ((finsuppTensorFinsuppLid R N ι κ).symm fun₀ | i => r • n) = (fun₀ | i.1 => r) ⊗ₜ[R] fun₀ | i.2 => n
• finsuppTensorFinsuppRid_symm_single_smul 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] (i : ι × κ) (m : M) (r : R) : ((finsuppTensorFinsuppRid R M ι κ).symm fun₀ | i => r • m) = (fun₀ | i.1 => m) ⊗ₜ[R] fun₀ | i.2 => r
• finsuppTensorFinsupp_single 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (i : ι) (m : M) (k : κ) (n : N) : (finsuppTensorFinsupp R S M N ι κ) ((fun₀ | i => m) ⊗ₜ[R] fun₀ | k => n) = fun₀ | (i, k) => m ⊗ₜ[R] n
• finsuppTensorFinsupp'_symm_single_eq_single_one_tmul 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] (i : ι × κ) (r : R) : ((finsuppTensorFinsupp' R ι κ).symm fun₀ | i => r) = (fun₀ | i.1 => 1) ⊗ₜ[R] fun₀ | i.2 => r
• finsuppTensorFinsupp'_symm_single_eq_tmul_single_one 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] (i : ι × κ) (r : R) : ((finsuppTensorFinsupp' R ι κ).symm fun₀ | i => r) = (fun₀ | i.1 => r) ⊗ₜ[R] fun₀ | i.2 => 1
• finsuppTensorFinsupp'_symm_single_mul 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] (i : ι × κ) (r₁ r₂ : R) : ((finsuppTensorFinsupp' R ι κ).symm fun₀ | i => r₁ * r₂) = (fun₀ | i.1 => r₁) ⊗ₜ[R] fun₀ | i.2 => r₂
• finsuppTensorFinsupp_apply 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (f : ι →₀ M) (g : κ →₀ N) (i : ι) (k : κ) : ((finsuppTensorFinsupp R S M N ι κ) (f ⊗ₜ[R] g)) (i, k) = f i ⊗ₜ[R] g k
• finsuppTensorFinsupp_symm_single 📋 Mathlib.LinearAlgebra.DirectSum.Finsupp
  (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (i : ι × κ) (m : M) (n : N) : ((finsuppTensorFinsupp R S M N ι κ).symm fun₀ | i => m ⊗ₜ[R] n) = (fun₀ | i.1 => m) ⊗ₜ[R] fun₀ | i.2 => n
• Module.Basis.tensorProduct 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
  {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Module.Basis ι S M) (c : Module.Basis κ R N) : Module.Basis (ι × κ) S (TensorProduct R M N)
• Module.Basis.tensorProduct_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
  {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Module.Basis ι S M) (c : Module.Basis κ R N) (i : ι) (j : κ) : (b.tensorProduct c) (i, j) = b i ⊗ₜ[R] c j
• Module.Basis.tensorProduct_apply' 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
  {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Module.Basis ι S M) (c : Module.Basis κ R N) (i : ι × κ) : (b.tensorProduct c) i = b i.1 ⊗ₜ[R] c i.2
• Module.Basis.tensorProduct_repr_tmul_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Basis
  {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] (b : Module.Basis ι S M) (c : Module.Basis κ R N) (m : M) (n : N) (i : ι) (j : κ) : ((b.tensorProduct c).repr (m ⊗ₜ[R] n)) (i, j) = (c.repr n) j • (b.repr m) i
• Algebra.TensorProduct.liftEquiv 📋 Mathlib.RingTheory.TensorProduct.Maps
  {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra S C] [Algebra R C] [IsScalarTower R S C] : { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) } ≃ (TensorProduct R A B →ₐ[S] C)
• Algebra.TensorProduct.liftEquiv_apply 📋 Mathlib.RingTheory.TensorProduct.Maps
  {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra S C] [Algebra R C] [IsScalarTower R S C] (fg : { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) }) : Algebra.TensorProduct.liftEquiv fg = Algebra.TensorProduct.lift (↑fg).1 (↑fg).2 ⋯
• Algebra.TensorProduct.liftEquiv_symm_apply_coe 📋 Mathlib.RingTheory.TensorProduct.Maps
  {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Semiring B] [Algebra R B] [Semiring C] [Algebra S C] [Algebra R C] [IsScalarTower R S C] (f' : TensorProduct R A B →ₐ[S] C) : ↑(Algebra.TensorProduct.liftEquiv.symm f') = (f'.comp Algebra.TensorProduct.includeLeft, (AlgHom.restrictScalars R f').comp Algebra.TensorProduct.includeRight)
• TensorProduct.exists_finset 📋 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] (x : TensorProduct R M N) : ∃ S, x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
• TensorProduct.exists_multiset 📋 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] (x : TensorProduct R M N) : ∃ S, x = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum
• LinearIndependent.tmul_of_flat_left 📋 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] {ι : Type u_6} {κ : Type u_7} {v : ι → M} {w : κ → N} [Module.Flat R M] (hv : LinearIndependent R v) (hw : LinearIndependent R w) : LinearIndependent R fun i => v i.1 ⊗ₜ[R] w i.2
• LinearIndependent.tmul_of_flat_right 📋 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] {ι : Type u_6} {κ : Type u_7} {v : ι → M} {w : κ → N} [Module.Flat R N] (hv : LinearIndependent R v) (hw : LinearIndependent R w) : LinearIndependent R fun i => v i.1 ⊗ₜ[R] w i.2
• TensorProduct.LinearIndepOn.tmul_of_flat_left 📋 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] {ι : Type u_6} {κ : Type u_7} {v : ι → M} {w : κ → N} {s : Set ι} {t : Set κ} [Module.Flat R M] (hv : LinearIndepOn R v s) (hw : LinearIndepOn R w t) : LinearIndepOn R (fun i => v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t)
• TensorProduct.LinearIndepOn.tmul_of_flat_right 📋 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] {ι : Type u_6} {κ : Type u_7} {v : ι → M} {w : κ → N} {s : Set ι} {t : Set κ} [Module.Flat R N] (hv : LinearIndepOn R v s) (hw : LinearIndepOn R w t) : LinearIndepOn R (fun i => v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t)
• 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
• 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
• 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)
• Coalgebra.Repr.tmul 📋 Mathlib.RingTheory.Bialgebra.TensorProduct
  {R : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} {κ : Type u_5} [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] {a : A} {b : B} (ℛa : Coalgebra.Repr R a ι) (ℛb : Coalgebra.Repr R b κ) : Coalgebra.Repr R (a ⊗ₜ[R] b) (ι × κ)
• Coalgebra.Repr.tmul_index 📋 Mathlib.RingTheory.Bialgebra.TensorProduct
  {R : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} {κ : Type u_5} [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] {a : A} {b : B} (ℛa : Coalgebra.Repr R a ι) (ℛb : Coalgebra.Repr R b κ) : (ℛa.tmul ℛb).index = ℛa.index ×ˢ ℛb.index
• Coalgebra.Repr.tmul_left 📋 Mathlib.RingTheory.Bialgebra.TensorProduct
  {R : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} {κ : Type u_5} [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] {a : A} {b : B} (ℛa : Coalgebra.Repr R a ι) (ℛb : Coalgebra.Repr R b κ) (i : ι × κ) : (ℛa.tmul ℛb).left i = ℛa.left i.1 ⊗ₜ[R] ℛb.left i.2
• Coalgebra.Repr.tmul_right 📋 Mathlib.RingTheory.Bialgebra.TensorProduct
  {R : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} {κ : Type u_5} [CommSemiring R] [Semiring A] [Bialgebra R A] [Semiring B] [Bialgebra R B] {a : A} {b : B} (ℛa : Coalgebra.Repr R a ι) (ℛb : Coalgebra.Repr R b κ) (i : ι × κ) : (ℛa.tmul ℛb).right i = ℛa.right i.1 ⊗ₜ[R] ℛb.right i.2
• dualTensorHom_prodMap_zero 📋 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) : ((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 = (dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ LinearMap.fst R M N) ⊗ₜ[R] (LinearMap.inl R P Q) p)
• zero_prodMap_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] (g : Module.Dual R N) (q : Q) : LinearMap.prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) = (dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ LinearMap.snd R M N) ⊗ₜ[R] (LinearMap.inr R P Q) q)
• CharacterModule.homEquiv_apply_apply 📋 Mathlib.Algebra.Module.CharacterModule
  {R : Type uR} [CommRing R] {A : Type uA} [AddCommGroup A] {B : Type uB} [AddCommGroup B] [Module R A] [Module R B] (c : A →ₗ[R] CharacterModule B) (x : (addConGen (TensorProduct.Eqv R A B)).Quotient) : (CharacterModule.homEquiv c) x = AddCon.liftOn x ⇑(FreeAddMonoid.lift fun mn => (c.toAddMonoidHom mn.1) mn.2) ⋯
• Matrix.kroneckerTMul 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] : Matrix l m α → Matrix n p β → Matrix (l × n) (m × p) (TensorProduct R α β)
• Matrix.trace_kroneckerTMul 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {m : Type u_10} {n : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Fintype m] [Fintype n] (A : Matrix m m α) (B : Matrix n n β) : (Matrix.kroneckerMap (TensorProduct.tmul R) A B).trace = A.trace ⊗ₜ[R] B.trace
• Matrix.kroneckerTMul_diagonal 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [DecidableEq n] (A : Matrix l m α) (b : n → β) : Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.diagonal b) = Matrix.blockDiagonal fun i => A.map fun a => a ⊗ₜ[R] b i
• Matrix.kroneckerTMul_zero 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (A : Matrix l m α) : Matrix.kroneckerMap (TensorProduct.tmul R) A 0 = 0
• Matrix.zero_kroneckerTMul 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (B : Matrix n p β) : Matrix.kroneckerMap (TensorProduct.tmul R) 0 B = 0
• Matrix.diagonal_kroneckerTMul_diagonal 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {m : Type u_10} {n : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [DecidableEq m] [DecidableEq n] (a : m → α) (b : n → β) : Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.diagonal a) (Matrix.diagonal b) = Matrix.diagonal fun mn => a mn.1 ⊗ₜ[R] b mn.2
• Matrix.single_kroneckerTMul_single 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (i₁ : l) (j₁ : m) (i₂ : n) (j₂ : p) (a : α) (b : β) : Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.single i₁ j₁ a) (Matrix.single i₂ j₂ b) = Matrix.single (i₁, i₂) (j₁, j₂) (a ⊗ₜ[R] b)
• Matrix.one_kroneckerTMul_one 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {m : Type u_10} {n : Type u_11} [CommSemiring R] [AddCommMonoidWithOne α] [AddCommMonoidWithOne β] [Module R α] [Module R β] [DecidableEq m] [DecidableEq n] : Matrix.kroneckerMap (TensorProduct.tmul R) 1 1 = 1
• Matrix.add_kroneckerTMul 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [Module R α] (A₁ A₂ : Matrix l m α) (B : Matrix n p α) : Matrix.kroneckerMap (TensorProduct.tmul R) (A₁ + A₂) B = Matrix.kroneckerMap (TensorProduct.tmul R) A₁ B + Matrix.kroneckerMap (TensorProduct.tmul R) A₂ B
• Matrix.kroneckerTMul_add 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (A : Matrix l m α) (B₁ B₂ : Matrix n p β) : Matrix.kroneckerMap (TensorProduct.tmul R) A (B₁ + B₂) = Matrix.kroneckerMap (TensorProduct.tmul R) A B₁ + Matrix.kroneckerMap (TensorProduct.tmul R) A B₂
• Matrix.smul_kroneckerTMul 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {S : Type u_2} {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Monoid S] [DistribMulAction S α] [SMulCommClass R S α] (r : S) (A : Matrix l m α) (B : Matrix n p β) : Matrix.kroneckerMap (TensorProduct.tmul R) (r • A) B = r • Matrix.kroneckerMap (TensorProduct.tmul R) A B
• Matrix.conjTranspose_kroneckerTMul 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [StarRing R] [StarAddMonoid α] [StarAddMonoid β] [StarModule R α] [StarModule R β] (x : Matrix l m α) (y : Matrix n p β) : (Matrix.kroneckerMap (TensorProduct.tmul R) x y).conjTranspose = Matrix.kroneckerMap (TensorProduct.tmul R) x.conjTranspose y.conjTranspose
• Matrix.diagonal_kroneckerTMul 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [DecidableEq l] (a : l → α) (B : Matrix m n β) : Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.diagonal a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun i => B.map fun b => a i ⊗ₜ[R] b)
• Matrix.det_kroneckerTMul 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {m : Type u_10} {n : Type u_11} [CommRing R] [CommRing α] [CommRing β] [Algebra R α] [Algebra R β] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m m α) (B : Matrix n n β) : (Matrix.kroneckerMap (TensorProduct.tmul R) A B).det = (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
• Matrix.kroneckerTMul_smul 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {S : Type u_2} {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Monoid S] [DistribMulAction S α] [DistribMulAction S β] [SMul S R] [SMulCommClass R S α] [IsScalarTower S R α] [IsScalarTower S R β] (r : S) (A : Matrix l m α) (B : Matrix n p β) : Matrix.kroneckerMap (TensorProduct.tmul R) A (r • B) = r • Matrix.kroneckerMap (TensorProduct.tmul R) A B
• Matrix.kroneckerTMulBilinear 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) (S : Type u_2) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Semiring S] [Module S α] [SMulCommClass R S α] : Matrix l m α →ₗ[S] Matrix n p β →ₗ[R] Matrix (l × n) (m × p) (TensorProduct R α β)
• Matrix.mul_kroneckerTMul_mul 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {l' : Type u_15} {m' : Type u_16} {n' : Type u_17} [CommSemiring R] [NonUnitalSemiring α] [NonUnitalSemiring β] [Module R α] [Module R β] [IsScalarTower R α α] [SMulCommClass R α α] [IsScalarTower R β β] [SMulCommClass R β β] [Fintype m] [Fintype m'] (A : Matrix l m α) (B : Matrix m n α) (A' : Matrix l' m' β) (B' : Matrix m' n' β) : Matrix.kroneckerMap (TensorProduct.tmul R) (A * B) (A' * B') = Matrix.kroneckerMap (TensorProduct.tmul R) A A' * Matrix.kroneckerMap (TensorProduct.tmul R) B B'
• Matrix.kroneckerTMul_assoc' 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} {q : Type u_13} {r : Type u_14} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) : ((Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.kroneckerMap (TensorProduct.tmul R) A B) C).map ⇑(TensorProduct.assoc R α β γ)).submatrix ⇑(Equiv.prodAssoc l n q).symm ⇑(Equiv.prodAssoc m p r).symm = Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.kroneckerMap (TensorProduct.tmul R) B C)
• Matrix.kroneckerTMul_assoc 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} {q : Type u_13} {r : Type u_14} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) : (Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)) ((Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.kroneckerMap (TensorProduct.tmul R) A B) C).map ⇑(TensorProduct.assoc R α β γ)) = Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.kroneckerMap (TensorProduct.tmul R) B C)
• Matrix.kroneckerTMulBilinear_apply 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  (R : Type u_1) {S : Type u_2} {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Semiring S] [Module S α] [SMulCommClass R S α] (A : Matrix l m α) (B : Matrix n p β) : ((Matrix.kroneckerTMulBilinear R S) A) B = Matrix.kroneckerMap (TensorProduct.tmul R) A B
• Matrix.kroneckerAlgEquiv 📋 Mathlib.RingTheory.MatrixAlgebra
  (m : Type u_2) (n : Type u_3) (R : Type u_5) [CommSemiring R] [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] : TensorProduct R (Matrix m m R) (Matrix n n R) ≃ₐ[R] Matrix (m × n) (m × n) R
• kroneckerLinearEquiv 📋 Mathlib.RingTheory.MatrixAlgebra
  (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) [CommSemiring R] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] : TensorProduct R (Matrix l m R) (Matrix n p R) ≃ₗ[R] Matrix (l × n) (m × p) R
• Matrix.kroneckerTMulAlgEquiv 📋 Mathlib.RingTheory.MatrixAlgebra
  (m : Type u_2) (n : Type u_3) (R : Type u_5) (S : Type u_6) (A : Type u_7) (B : Type u_8) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] [Fintype m] [DecidableEq m] : TensorProduct R (Matrix m m A) (Matrix n n B) ≃ₐ[S] Matrix (m × n) (m × n) (TensorProduct R A B)
• kroneckerTMulLinearEquiv 📋 Mathlib.RingTheory.MatrixAlgebra
  (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9) (N : Type u_10) [CommSemiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Module R M] [Module S M] [Module R N] [IsScalarTower R S M] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] : TensorProduct R (Matrix l m M) (Matrix n p N) ≃ₗ[S] Matrix (l × n) (m × p) (TensorProduct R M N)
• matrixEquivTensor_apply 📋 Mathlib.RingTheory.MatrixAlgebra
  (n : Type u_3) (R : Type u_5) (A : Type u_7) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] (M : Matrix n n A) : (matrixEquivTensor n R A) M = ∑ p, M p.1 p.2 ⊗ₜ[R] Matrix.single p.1 p.2 1
• Matrix.toLinearEquiv_kroneckerAlgEquiv 📋 Mathlib.RingTheory.MatrixAlgebra
  {m : Type u_2} {n : Type u_3} (R : Type u_5) [CommSemiring R] [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] : ↑(Matrix.kroneckerAlgEquiv m n R) = kroneckerLinearEquiv m m n n R
• Matrix.kroneckerStarAlgEquiv 📋 Mathlib.RingTheory.MatrixAlgebra
  (m : Type u_2) (n : Type u_3) (R : Type u_5) [CommSemiring R] [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [StarRing R] : TensorProduct R (Matrix m m R) (Matrix n n R) ≃⋆ₐ[R] Matrix (m × n) (m × n) R
• Matrix.toAlgEquiv_kroneckerStarAlgEquiv 📋 Mathlib.RingTheory.MatrixAlgebra
  {m : Type u_2} {n : Type u_3} (R : Type u_5) [CommSemiring R] [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [StarRing R] : (Matrix.kroneckerStarAlgEquiv m n R).toAlgEquiv = Matrix.kroneckerAlgEquiv m n R
• kroneckerLinearEquiv_tmul 📋 Mathlib.RingTheory.MatrixAlgebra
  {l : Type u_1} {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_5} [CommSemiring R] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (x : Matrix l m R) (y : Matrix n p R) : (kroneckerLinearEquiv l m n p R) (x ⊗ₜ[R] y) = Matrix.kroneckerMap (fun x1 x2 => x1 * x2) x y
• Matrix.kroneckerTMulStarAlgEquiv 📋 Mathlib.RingTheory.MatrixAlgebra
  (m : Type u_2) (n : Type u_3) (R : Type u_5) (S : Type u_6) (A : Type u_7) (B : Type u_8) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] [Fintype m] [DecidableEq m] [StarRing R] [StarAddMonoid A] [StarAddMonoid B] [StarModule R A] [StarModule R B] : TensorProduct R (Matrix m m A) (Matrix n n B) ≃⋆ₐ[S] Matrix (m × n) (m × n) (TensorProduct R A B)
• Matrix.toAlgEquiv_kroneckerTMulStarAlgEquiv 📋 Mathlib.RingTheory.MatrixAlgebra
  {m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] [Fintype m] [DecidableEq m] [StarRing R] [StarAddMonoid A] [StarAddMonoid B] [StarModule R A] [StarModule R B] : (Matrix.kroneckerTMulStarAlgEquiv m n R S A B).toAlgEquiv = Matrix.kroneckerTMulAlgEquiv m n R S A B
• kroneckerTMulLinearEquiv_tmul 📋 Mathlib.RingTheory.MatrixAlgebra
  (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9) (N : Type u_10) [CommSemiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Module R M] [Module S M] [Module R N] [IsScalarTower R S M] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (a : Matrix l m M) (b : Matrix n p N) : (kroneckerTMulLinearEquiv l m n p R S M N) (a ⊗ₜ[R] b) = Matrix.kroneckerMap (TensorProduct.tmul R) a b
• kroneckerLinearEquiv_symm_kronecker 📋 Mathlib.RingTheory.MatrixAlgebra
  {l : Type u_1} {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_5} [CommSemiring R] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (x : Matrix l m R) (y : Matrix n p R) : (kroneckerLinearEquiv l m n p R).symm (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) x y) = x ⊗ₜ[R] y
• kroneckerTMulLinearEquiv_symm_kroneckerTMul 📋 Mathlib.RingTheory.MatrixAlgebra
  (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9) (N : Type u_10) [CommSemiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Module R M] [Module S M] [Module R N] [IsScalarTower R S M] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (a : Matrix l m M) (b : Matrix n p N) : (kroneckerTMulLinearEquiv l m n p R S M N).symm (Matrix.kroneckerMap (TensorProduct.tmul R) a b) = a ⊗ₜ[R] b
• Matrix.kroneckerAlgEquiv_apply 📋 Mathlib.RingTheory.MatrixAlgebra
  {m : Type u_2} {n : Type u_3} (R : Type u_5) [CommSemiring R] [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] (x : TensorProduct R (Matrix m m R) (Matrix n n R)) : (Matrix.kroneckerAlgEquiv m n R) x = (kroneckerLinearEquiv m m n n R) x
• kroneckerTMulAlgEquiv_symm_single_tmul 📋 Mathlib.RingTheory.MatrixAlgebra
  (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (S : Type u_6) (M : Type u_9) (N : Type u_10) [CommSemiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Module R M] [Module S M] [Module R N] [IsScalarTower R S M] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (ia : l) (ja : m) (ib : n) (jb : p) (a : M) (b : N) : (kroneckerTMulLinearEquiv l m n p R S M N).symm (Matrix.single (ia, ib) (ja, jb) (a ⊗ₜ[R] b)) = Matrix.single ia ja a ⊗ₜ[R] Matrix.single ib jb b
• Matrix.kroneckerAlgEquiv_symm_apply 📋 Mathlib.RingTheory.MatrixAlgebra
  {m : Type u_2} {n : Type u_3} (R : Type u_5) [CommSemiring R] [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] (x : Matrix (m × n) (m × n) R) : (Matrix.kroneckerAlgEquiv m n R).symm x = (kroneckerLinearEquiv m m n n R).symm x
• kroneckerTMulLinearEquiv_one 📋 Mathlib.RingTheory.MatrixAlgebra
  (m : Type u_2) (n : Type u_3) (R : Type u_5) (S : Type u_6) (A : Type u_7) {B : Type u_8} [CommSemiring R] [Semiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [Module S A] [IsScalarTower R S A] : (kroneckerTMulLinearEquiv m m n n R S A B) 1 = 1
• Matrix.kroneckerStarAlgEquiv_apply 📋 Mathlib.RingTheory.MatrixAlgebra
  {m : Type u_2} {n : Type u_3} (R : Type u_5) [CommSemiring R] [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [StarRing R] (x : TensorProduct R (Matrix m m R) (Matrix n n R)) : (Matrix.kroneckerStarAlgEquiv m n R) x = (kroneckerLinearEquiv m m n n R) x
• Matrix.kroneckerTMulAlgEquiv_apply 📋 Mathlib.RingTheory.MatrixAlgebra
  {m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] [Fintype m] [DecidableEq m] (x : TensorProduct R (Matrix m m A) (Matrix n n B)) : (Matrix.kroneckerTMulAlgEquiv m n R S A B) x = (kroneckerTMulLinearEquiv m m n n R S A B) x
• Matrix.kroneckerStarAlgEquiv_symm_apply 📋 Mathlib.RingTheory.MatrixAlgebra
  {m : Type u_2} {n : Type u_3} (R : Type u_5) [CommSemiring R] [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [StarRing R] (x : Matrix (m × n) (m × n) R) : (Matrix.kroneckerStarAlgEquiv m n R).symm x = (kroneckerLinearEquiv m m n n R).symm x
• Matrix.kroneckerTMulAlgEquiv_symm_apply 📋 Mathlib.RingTheory.MatrixAlgebra
  {m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] [Fintype m] [DecidableEq m] (x : Matrix (m × n) (m × n) (TensorProduct R A B)) : (Matrix.kroneckerTMulAlgEquiv m n R S A B).symm x = (kroneckerTMulLinearEquiv m m n n R S A B).symm x
• Matrix.kroneckerTMulStarAlgEquiv_apply 📋 Mathlib.RingTheory.MatrixAlgebra
  {m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] [Fintype m] [DecidableEq m] [StarRing R] [StarAddMonoid A] [StarAddMonoid B] [StarModule R A] [StarModule R B] (x : TensorProduct R (Matrix m m A) (Matrix n n B)) : (Matrix.kroneckerTMulStarAlgEquiv m n R S A B) x = (kroneckerTMulLinearEquiv m m n n R S A B) x
• Matrix.kroneckerTMulStarAlgEquiv_symm_apply 📋 Mathlib.RingTheory.MatrixAlgebra
  {m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [CommSemiring S] [Algebra R S] [Algebra S A] [IsScalarTower R S A] [Fintype m] [DecidableEq m] [StarRing R] [StarAddMonoid A] [StarAddMonoid B] [StarModule R A] [StarModule R B] (x : Matrix (m × n) (m × n) (TensorProduct R A B)) : (Matrix.kroneckerTMulStarAlgEquiv m n R S A B).symm x = (kroneckerTMulLinearEquiv m m n n R S A B).symm x
• kroneckerTMulLinearEquiv_mul 📋 Mathlib.RingTheory.MatrixAlgebra
  (m : Type u_2) (n : Type u_3) (R : Type u_5) (S : Type u_6) (A : Type u_7) {B : Type u_8} [CommSemiring R] [Semiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [Module S A] [IsScalarTower R S A] (x y : TensorProduct R (Matrix m m A) (Matrix n n B)) : (kroneckerTMulLinearEquiv m m n n R S A B) (x * y) = (kroneckerTMulLinearEquiv m m n n R S A B) x * (kroneckerTMulLinearEquiv m m n n R S A B) y
• AddMonoidAlgebra.tensorEquiv 📋 Mathlib.RingTheory.TensorProduct.MonoidAlgebra
  (R : Type u_1) {M : Type u_2} {N : Type u_3} [CommSemiring R] : TensorProduct R (AddMonoidAlgebra R M) (AddMonoidAlgebra R N) ≃ₗ[R] AddMonoidAlgebra R (M × N)
• MonoidAlgebra.tensorEquiv 📋 Mathlib.RingTheory.TensorProduct.MonoidAlgebra
  (R : Type u_1) {M : Type u_2} {N : Type u_3} [CommSemiring R] : TensorProduct R (MonoidAlgebra R M) (MonoidAlgebra R N) ≃ₗ[R] MonoidAlgebra R (M × N)
• AddMonoidAlgebra.tensorEquiv_single_tmul_single 📋 Mathlib.RingTheory.TensorProduct.MonoidAlgebra
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] (m : M) (r₁ : R) (n : N) (r₂ : R) : (AddMonoidAlgebra.tensorEquiv R) (AddMonoidAlgebra.single m r₁ ⊗ₜ[R] AddMonoidAlgebra.single n r₂) = AddMonoidAlgebra.single (m, n) (r₁ * r₂)
• MonoidAlgebra.tensorEquiv_single_tmul_single 📋 Mathlib.RingTheory.TensorProduct.MonoidAlgebra
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] (m : M) (r₁ : R) (n : N) (r₂ : R) : (MonoidAlgebra.tensorEquiv R) (MonoidAlgebra.single m r₁ ⊗ₜ[R] MonoidAlgebra.single n r₂) = MonoidAlgebra.single (m, n) (r₁ * r₂)
• AddMonoidAlgebra.tensorEquiv_symm_single_eq_single_zero_tmul 📋 Mathlib.RingTheory.TensorProduct.MonoidAlgebra
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] (mn : M × N) (r : R) : (AddMonoidAlgebra.tensorEquiv R).symm (AddMonoidAlgebra.single mn r) = AddMonoidAlgebra.single mn.1 1 ⊗ₜ[R] AddMonoidAlgebra.single mn.2 r
• AddMonoidAlgebra.tensorEquiv_symm_single_eq_tmul_single_zero 📋 Mathlib.RingTheory.TensorProduct.MonoidAlgebra
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] (mn : M × N) (r : R) : (AddMonoidAlgebra.tensorEquiv R).symm (AddMonoidAlgebra.single mn r) = AddMonoidAlgebra.single mn.1 r ⊗ₜ[R] AddMonoidAlgebra.single mn.2 1
• MonoidAlgebra.tensorEquiv_symm_single_eq_single_one_tmul 📋 Mathlib.RingTheory.TensorProduct.MonoidAlgebra
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] (mn : M × N) (r : R) : (MonoidAlgebra.tensorEquiv R).symm (MonoidAlgebra.single mn r) = MonoidAlgebra.single mn.1 1 ⊗ₜ[R] MonoidAlgebra.single mn.2 r
• MonoidAlgebra.tensorEquiv_symm_single_eq_tmul_single_one 📋 Mathlib.RingTheory.TensorProduct.MonoidAlgebra
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] (mn : M × N) (r : R) : (MonoidAlgebra.tensorEquiv R).symm (MonoidAlgebra.single mn r) = MonoidAlgebra.single mn.1 r ⊗ₜ[R] MonoidAlgebra.single mn.2 1
• AddMonoidAlgebra.coeff_tensorEquiv_apply 📋 Mathlib.RingTheory.TensorProduct.MonoidAlgebra
  (R : Type u_1) {M : Type u_2} {N : Type u_3} [CommSemiring R] (x : TensorProduct R (AddMonoidAlgebra R M) (AddMonoidAlgebra R N)) : ((AddMonoidAlgebra.tensorEquiv R) x).coeff = (finsuppTensorFinsupp' R M N) ((TensorProduct.congr (AddMonoidAlgebra.coeffLinearEquiv R) (AddMonoidAlgebra.coeffLinearEquiv R)) x)
• MonoidAlgebra.coeff_tensorEquiv_apply 📋 Mathlib.RingTheory.TensorProduct.MonoidAlgebra
  (R : Type u_1) {M : Type u_2} {N : Type u_3} [CommSemiring R] (x : TensorProduct R (MonoidAlgebra R M) (MonoidAlgebra R N)) : ((MonoidAlgebra.tensorEquiv R) x).coeff = (finsuppTensorFinsupp' R M N) ((TensorProduct.congr (MonoidAlgebra.coeffLinearEquiv R) (MonoidAlgebra.coeffLinearEquiv R)) x)
• TensorProduct.prodRight 📋 Mathlib.LinearAlgebra.TensorProduct.Prod
  (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] : TensorProduct R M₁ (M₂ × M₃) ≃ₗ[S] TensorProduct R M₁ M₂ × TensorProduct R M₁ M₃
• TensorProduct.prodLeft 📋 Mathlib.LinearAlgebra.TensorProduct.Prod
  (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] [Module S M₂] [IsScalarTower R S M₂] : TensorProduct R (M₁ × M₂) M₃ ≃ₗ[S] TensorProduct R M₁ M₃ × TensorProduct R M₂ M₃
• TensorProduct.prodRight_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Prod
  (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m : M₂ × M₃) : (TensorProduct.prodRight R S M₁ M₂ M₃) (m₁ ⊗ₜ[R] m) = (m₁ ⊗ₜ[R] m.1, m₁ ⊗ₜ[R] m.2)
• TensorProduct.prodRight_symm_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Prod
  (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : (TensorProduct.prodRight R S M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₂, m₁ ⊗ₜ[R] m₃) = m₁ ⊗ₜ[R] (m₂, m₃)
• TensorProduct.prodLeft_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Prod
  (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] [Module S M₂] [IsScalarTower R S M₂] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : (TensorProduct.prodLeft R S M₁ M₂ M₃) ((m₁, m₂) ⊗ₜ[R] m₃) = (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃)
• TensorProduct.prodLeft_symm_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Prod
  (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [CommSemiring R] [Semiring S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [Algebra R S] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] [Module R M₂] [Module R M₃] [Module S M₂] [IsScalarTower R S M₂] (m₁ : M₁) (m₂ : M₂) (m₃ : M₃) : (TensorProduct.prodLeft R S M₁ M₂ M₃).symm (m₁ ⊗ₜ[R] m₃, m₂ ⊗ₜ[R] m₃) = (m₁, m₂) ⊗ₜ[R] m₃
• Algebra.TensorProduct.prodRight 📋 Mathlib.RingTheory.TensorProduct.Pi
  (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] : TensorProduct R A (B × C) ≃ₐ[S] TensorProduct R A B × TensorProduct R A C
• Algebra.TensorProduct.prodRight_tmul_fst 📋 Mathlib.RingTheory.TensorProduct.Pi
  (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] (a : A) (x : B × C) : ((Algebra.TensorProduct.prodRight R S A B C) (a ⊗ₜ[R] x)).1 = a ⊗ₜ[R] x.1
• Algebra.TensorProduct.prodRight_tmul_snd 📋 Mathlib.RingTheory.TensorProduct.Pi
  (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] (a : A) (x : B × C) : ((Algebra.TensorProduct.prodRight R S A B C) (a ⊗ₜ[R] x)).2 = a ⊗ₜ[R] x.2
• Algebra.TensorProduct.prodRight_tmul 📋 Mathlib.RingTheory.TensorProduct.Pi
  (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] (a : A) (x : B × C) : (Algebra.TensorProduct.prodRight R S A B C) (a ⊗ₜ[R] x) = (a ⊗ₜ[R] x.1, a ⊗ₜ[R] x.2)
• Algebra.TensorProduct.prodRight_symm_tmul 📋 Mathlib.RingTheory.TensorProduct.Pi
  (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Algebra R S] [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (B : Type u_6) (C : Type u_7) [Semiring B] [Semiring C] [Algebra R B] [Algebra R C] (a : A) (b : B) (c : C) : (Algebra.TensorProduct.prodRight R S A B C).symm (a ⊗ₜ[R] b, a ⊗ₜ[R] c) = a ⊗ₜ[R] (b, c)
• Module.Basis.baseChange_end 📋 Mathlib.RingTheory.TensorProduct.Free
  {R : Type u_1} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (A : Type u_5) [CommSemiring A] [Algebra R A] [DecidableEq ι] (b : Module.Basis ι R M) (ij : ι × ι) : LinearMap.baseChange A (b.end ij) = (Algebra.TensorProduct.basis A b).end ij
• Module.Basis.baseChange_linearMap 📋 Mathlib.RingTheory.TensorProduct.Free
  {R : Type u_1} {M : Type uM} {ι : Type uι} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] {ι' : Type u_3} {N : Type u_4} [Fintype ι'] [DecidableEq ι'] [AddCommMonoid N] [Module R N] (A : Type u_5) [CommSemiring A] [Algebra R A] (b : Module.Basis ι R M) (b' : Module.Basis ι' R N) (ij : ι × ι') : LinearMap.baseChange A ((b'.linearMap b) ij) = ((Algebra.TensorProduct.basis A b').linearMap (Algebra.TensorProduct.basis A b)) ij
• Module.Presentation.tensor_G 📋 Mathlib.Algebra.Module.Presentation.Tensor
  {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (pres₁ : Module.Presentation A M₁) (pres₂ : Module.Presentation A M₂) : (pres₁.tensor pres₂).G = (pres₁.G × pres₂.G)
• Module.Presentation.tensor_R 📋 Mathlib.Algebra.Module.Presentation.Tensor
  {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (pres₁ : Module.Presentation A M₁) (pres₂ : Module.Presentation A M₂) : (pres₁.tensor pres₂).R = (pres₁.R × pres₂.G ⊕ pres₁.G × pres₂.R)
• Module.Presentation.tensor_var 📋 Mathlib.Algebra.Module.Presentation.Tensor
  {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (pres₁ : Module.Presentation A M₁) (pres₂ : Module.Presentation A M₂) (x✝ : (pres₁.tensor pres₂.toRelations).G) : (pres₁.tensor pres₂).var x✝ = match x✝ with | (g₁, g₂) => pres₁.var g₁ ⊗ₜ[A] pres₂.var g₂
• Module.Presentation.tensor_relation 📋 Mathlib.Algebra.Module.Presentation.Tensor
  {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (pres₁ : Module.Presentation A M₁) (pres₂ : Module.Presentation A M₂) (x✝ : pres₁.R × pres₂.G ⊕ pres₁.G × pres₂.R) : (pres₁.tensor pres₂).relation x✝ = match x✝ with | Sum.inl (r₁, g₂) => Finsupp.embDomain (Function.Embedding.sectL pres₁.G g₂) (pres₁.relation r₁) | Sum.inr (g₁, r₂) => Finsupp.embDomain (Function.Embedding.sectR g₁ pres₂.G) (pres₂.relation r₂)
• PrimeSpectrum.tensorProductTo 📋 Mathlib.RingTheory.Spectrum.Prime.TensorProduct
  (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] (x : PrimeSpectrum (TensorProduct R S T)) : PrimeSpectrum S × PrimeSpectrum T
• PrimeSpectrum.continuous_tensorProductTo 📋 Mathlib.RingTheory.Spectrum.Prime.TensorProduct
  (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] : Continuous (PrimeSpectrum.tensorProductTo R S T)
• PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks 📋 Mathlib.RingTheory.Spectrum.Prime.TensorProduct
  (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] (hRT : (algebraMap R T).SurjectiveOnStalks) : Topology.IsEmbedding (PrimeSpectrum.tensorProductTo R S T)
• PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux 📋 Mathlib.RingTheory.Spectrum.Prime.TensorProduct
  (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] (hRT : (algebraMap R T).SurjectiveOnStalks) (p₁ p₂ : PrimeSpectrum (TensorProduct R S T)) (h : PrimeSpectrum.tensorProductTo R S T p₁ = PrimeSpectrum.tensorProductTo R S T p₂) : p₁ ≤ p₂
• Algebra.FormallyUnramified.exists_algEquiv_prod 📋 Mathlib.RingTheory.Unramified.Basic
  (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] [Algebra.FormallyUnramified R S] : ∃ T x x_1, Nonempty (TensorProduct R S S ≃ₐ[S] S × T)
• Algebra.Generators.CotangentSpace.compEquiv 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
  {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) : (Q.comp P).toExtension.CotangentSpace ≃ₗ[T] Q.toExtension.CotangentSpace × TensorProduct S T P.toExtension.CotangentSpace
• Algebra.Generators.CotangentSpace.fst_compEquiv 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
  {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) : LinearMap.fst T Q.toExtension.CotangentSpace (TensorProduct S T P.toExtension.CotangentSpace) ∘ₗ ↑(Algebra.Generators.CotangentSpace.compEquiv Q P) = Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom
• Algebra.Generators.CotangentSpace.fst_compEquiv_apply 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
  {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) (x : (Q.comp P).toExtension.CotangentSpace) : ((Algebra.Generators.CotangentSpace.compEquiv Q P) x).1 = (Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) x
• Algebra.Generators.H1Cotangent.δAux_ofComp 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
  {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) (x : (Q.comp P).Ring) : (Algebra.Generators.H1Cotangent.δAux R Q) ((Q.ofComp P).toAlgHom x) = (LinearMap.baseChange T P.toExtension.toKaehler) ((Algebra.Generators.CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (KaehlerDifferential.D R (Q.comp P).Ring) x)).2
• Algebra.Generators.CotangentSpace.compEquiv_symm_inr 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
  {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) : ↑(Algebra.Generators.CotangentSpace.compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (TensorProduct S T P.toExtension.CotangentSpace) = LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)
• Algebra.Generators.CotangentSpace.compEquiv_symm_zero 📋 Mathlib.RingTheory.Kaehler.JacobiZariski
  {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] [Algebra R S] {T : Type u₃} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] {ι : Type w₁} {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) (x : TensorProduct S T P.toExtension.CotangentSpace) : (Algebra.Generators.CotangentSpace.compEquiv Q P).symm (0, x) = (LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) x
• Matrix.kroneckerTMul_mem_unitary 📋 Mathlib.LinearAlgebra.UnitaryGroup
  {n : Type u} [DecidableEq n] [Fintype n] {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [StarRing A] [StarRing B] [StarRing R] [StarModule R A] [StarModule R B] {m : Type u_4} [Fintype m] [DecidableEq m] {U : Matrix m m A} {V : Matrix n n B} (hU : U ∈ unitary (Matrix m m A)) (hV : V ∈ unitary (Matrix n n B)) : Matrix.kroneckerMap (TensorProduct.tmul R) U V ∈ unitary (Matrix (m × n) (m × n) (TensorProduct R A B))
• Algebra.Generators.cotangentCompLocalizationAwayEquiv 📋 Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
  {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Algebra.Generators R S ι) {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent} (hx : (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x = Algebra.Generators.cMulXSubOneCotangent T g) : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent ≃ₗ[T] TensorProduct S T P.toExtension.Cotangent × (Algebra.Generators.localizationAway T g).toExtension.Cotangent
• Algebra.Generators.snd_comp_cotangentCompLocalizationAwayEquiv 📋 Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
  {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Algebra.Generators R S ι) {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent} (hx : (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x = Algebra.Generators.cMulXSubOneCotangent T g) : LinearMap.snd T (TensorProduct S T P.toExtension.Cotangent) (Algebra.Generators.localizationAway T g).toExtension.Cotangent ∘ₗ ↑(Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx) = Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom
• Algebra.Generators.snd_cotangentCompLocalizationAwayEquiv 📋 Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
  {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Algebra.Generators R S ι) {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent} (hx : (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x = Algebra.Generators.cMulXSubOneCotangent T g) (a : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent) : ((Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx) a).2 = (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) a
• Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_comp_inl 📋 Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
  {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Algebra.Generators R S ι) {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent} (hx : (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x = Algebra.Generators.cMulXSubOneCotangent T g) : ↑(Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx).symm ∘ₗ LinearMap.inl T (TensorProduct S T P.toExtension.Cotangent) (Algebra.Generators.localizationAway T g).toExtension.Cotangent = LinearMap.liftBaseChange T (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).toComp P).toExtensionHom)
• Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_inr 📋 Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
  {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Algebra.Generators R S ι) {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent} (hx : (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x = Algebra.Generators.cMulXSubOneCotangent T g) : (Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx).symm (0, Algebra.Generators.cMulXSubOneCotangent T g) = x
• Algebra.Generators.cotangentCompLocalizationAwayEquiv_symm_inl 📋 Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
  {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : S) [IsLocalization.Away g T] (P : Algebra.Generators R S ι) {x : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent} (hx : (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x = Algebra.Generators.cMulXSubOneCotangent T g) (a : TensorProduct S T P.toExtension.Cotangent) : (Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx).symm (a, 0) = (LinearMap.liftBaseChange T (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).toComp P).toExtensionHom)) a
• MvPolynomial.universalFactorizationMapLiftEquiv 📋 Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
  (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (n m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq S n) : { f // f.comp (MvPolynomial.universalFactorizationMap R n m k hn) = (MvPolynomial.mapEquivMonic R S n).symm p } ≃ { q // ↑q.1 * ↑q.2 = ↑p }
• OrthonormalBasis.tensorProduct 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) : OrthonormalBasis (ι₁ × ι₂) 𝕜 (TensorProduct 𝕜 E F)
• Orthonormal.tmul 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} {b₁ : ι₁ → E} {b₂ : ι₂ → F} (hb₁ : Orthonormal 𝕜 b₁) (hb₂ : Orthonormal 𝕜 b₂) : Orthonormal 𝕜 fun i => b₁ i.1 ⊗ₜ[𝕜] b₂ i.2
• TensorProduct.continuous_tmul 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] : Continuous fun x => x.1 ⊗ₜ[𝕜] x.2
• OrthonormalBasis.tensorProduct_apply 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (i : ι₁) (j : ι₂) : (b₁.tensorProduct b₂) (i, j) = b₁ i ⊗ₜ[𝕜] b₂ j
• OrthonormalBasis.tensorProduct_apply' 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (i : ι₁ × ι₂) : (b₁.tensorProduct b₂) i = b₁ i.1 ⊗ₜ[𝕜] b₂ i.2
• OrthonormalBasis.toBasis_tensorProduct 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) : (b₁.tensorProduct b₂).toBasis = b₁.toBasis.tensorProduct b₂.toBasis
• Orthonormal.basisTensorProduct 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} {b₁ : Module.Basis ι₁ 𝕜 E} {b₂ : Module.Basis ι₂ 𝕜 F} (hb₁ : Orthonormal 𝕜 ⇑b₁) (hb₂ : Orthonormal 𝕜 ⇑b₂) : Orthonormal 𝕜 ⇑(b₁.tensorProduct b₂)
• OrthonormalBasis.tensorProduct_repr_tmul_apply 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (x : E) (y : F) (i : ι₁) (j : ι₂) : ((b₁.tensorProduct b₂).repr (x ⊗ₜ[𝕜] y)).ofLp (i, j) = (b₂.repr y).ofLp j * (b₁.repr x).ofLp i
• OrthonormalBasis.tensorProduct_repr_tmul_apply' 📋 Mathlib.Analysis.InnerProductSpace.TensorProduct
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_6} {ι₂ : Type u_7} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (x : E) (y : F) (i : ι₁ × ι₂) : ((b₁.tensorProduct b₂).repr (x ⊗ₜ[𝕜] y)).ofLp i = (b₂.repr y).ofLp i.2 * (b₁.repr x).ofLp i.1
• AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
  {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm.ModSumCongr ιa ιb) {v : ιa ⊕ ιb → Mᵢ} {i j : ιa ⊕ ιb} (hv : v i = v j) (hij : i ≠ j) : Equiv.swap i j • σ = σ → (AlternatingMap.domCoprod.summand a b σ) v = 0
• AlternatingMap.domCoprod_coe 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
  {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) : ↑(a.domCoprod b) = ∑ σ, AlternatingMap.domCoprod.summand a b σ
• AlternatingMap.domCoprod_apply 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
  {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (v : ιa ⊕ ιb → Mᵢ) : (a.domCoprod b) v = (∑ σ, AlternatingMap.domCoprod.summand a b σ) v
• AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
  {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm.ModSumCongr ιa ιb) {v : ιa ⊕ ιb → Mᵢ} {i j : ιa ⊕ ιb} (hv : v i = v j) (hij : i ≠ j) : (AlternatingMap.domCoprod.summand a b σ) v + (AlternatingMap.domCoprod.summand a b (Equiv.swap i j • σ)) v = 0
• AlternatingMap.domCoprod.summand_mk'' 📋 Mathlib.LinearAlgebra.Alternating.DomCoprod
  {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm (ιa ⊕ ιb)) : AlternatingMap.domCoprod.summand a b (Quotient.mk'' σ) = Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)
• TensorProduct.instModuleFstSnd 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
  {R : Type u_1} {ι : Type u_2} (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] (i : ι × ι) : Module R (TensorProduct R (𝒜 i.1) (ℬ i.2))
• TensorProduct.gradedCommAux 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
  (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] : (DirectSum (ι × ι) fun i => TensorProduct R (𝒜 i.1) (ℬ i.2)) →ₗ[R] DirectSum (ι × ι) fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)
• TensorProduct.gradedCommAux_comp_gradedCommAux 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
  (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] : TensorProduct.gradedCommAux R 𝒜 ℬ ∘ₗ TensorProduct.gradedCommAux R ℬ 𝒜 = LinearMap.id
• TensorProduct.gradedCommAux_lof_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Graded.External
  (R : Type u_1) {ι : Type u_2} [CommSemiring ι] [Module ι (Additive ℤˣ)] [DecidableEq ι] (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [CommRing R] [(i : ι) → AddCommGroup (𝒜 i)] [(i : ι) → AddCommGroup (ℬ i)] [(i : ι) → Module R (𝒜 i)] [(i : ι) → Module R (ℬ i)] (i j : ι) (a : 𝒜 i) (b : ℬ j) : (TensorProduct.gradedCommAux R 𝒜 ℬ) ((DirectSum.lof R (ι × ι) (fun i => TensorProduct R (𝒜 i.1) (ℬ i.2)) (i, j)) (a ⊗ₜ[R] b)) = (-1) ^ (j * i) • (DirectSum.lof R (ι × ι) (fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)) (j, i)) (b ⊗ₜ[R] a)
• TensorProduct.toMatrix_comm 📋 Mathlib.LinearAlgebra.TensorProduct.Matrix
  {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_7} {κ : Type u_8} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (bM : Module.Basis ι R M) (bN : Module.Basis κ R N) : (LinearMap.toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM)) ↑(TensorProduct.comm R M N) = Matrix.submatrix 1 Prod.swap id
• 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.toMatrix_assoc 📋 Mathlib.LinearAlgebra.TensorProduct.Matrix
  {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} {ι : Type u_7} {κ : Type u_8} {τ : Type u_9} [DecidableEq ι] [DecidableEq κ] [DecidableEq τ] [Fintype ι] [Fintype κ] [Fintype τ] [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (bM : Module.Basis ι R M) (bN : Module.Basis κ R N) (bP : Module.Basis τ R P) : (LinearMap.toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP))) ↑(TensorProduct.assoc R M N P) = Matrix.submatrix 1 id ⇑(Equiv.prodAssoc ι κ τ)
• ContinuousMap.tensorHom 📋 Mathlib.Topology.UniformSpace.ProdApproximation
  {X : Type u_5} {Y : Type u_6} {R : Type u_7} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] : TensorProduct R C(X, R) C(Y, R) →ₗ[R] C(X × Y, R)
• ContinuousMap.denseRange_tensorHom 📋 Mathlib.Topology.UniformSpace.ProdApproximation
  {X : Type u_5} {Y : Type u_6} {R : Type u_7} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace X] [T2Space X] [CompactSpace Y] [TotallyDisconnectedSpace X] : DenseRange ⇑ContinuousMap.tensorHom
• ContinuousMap.tensorHom_tmul 📋 Mathlib.Topology.UniformSpace.ProdApproximation
  {X : Type u_5} {Y : Type u_6} {R : Type u_7} [TopologicalSpace X] [TopologicalSpace Y] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (f : C(X, R)) (g : C(Y, R)) : ContinuousMap.tensorHom (f ⊗ₜ[R] g) = (ContinuousMap.prodMul f) g
• Representation.LinearizeMonoidal.μ_toLinearMap 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : (Representation.LinearizeMonoidal.μ X Y).toLinearMap = ↑(MonoidAlgebra.tensorEquiv k)
• LinearIndependent.tmul_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] {ι : Type u_6} {κ : Type u_7} {v : ι → M} {w : κ → N} (hv : LinearIndependent R v) (hw : LinearIndependent R w) : LinearIndependent R fun i => v i.1 ⊗ₜ[R] w i.2
• LinearIndepOn.tmul_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] {ι : Type u_6} {κ : Type u_7} {v : ι → M} {w : κ → N} {s : Set ι} {t : Set κ} (hv : LinearIndepOn R v s) (hw : LinearIndepOn R w t) : LinearIndepOn R (fun i => v i.1 ⊗ₜ[R] w i.2) (s ×ˢ t)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision c026161