Loogle!

Result

Found 121 declarations mentioning Representation.tprod.

• Representation.tprod 📋 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) : Representation k G (TensorProduct k V W)
• 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.smul_one_tprod_asModule 📋 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] (ρW : Representation k G W) (r : MonoidAlgebra k G) (x : V) (y : W) : (r • have this := x ⊗ₜ[k] y; this) = x ⊗ₜ[k] (r • have this := y; this)
• Representation.smul_tprod_one_asModule 📋 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) (r : MonoidAlgebra k G) (x : V) (y : W) : (r • have this := x ⊗ₜ[k] y; this) = (r • have this := x; this) ⊗ₜ[k] y
• Representation.TensorProduct.lid 📋 Mathlib.RepresentationTheory.Intertwining
  (A : Type u_1) {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) : ((Representation.trivial A G A).tprod σ).Equiv σ
• Representation.TensorProduct.rid 📋 Mathlib.RepresentationTheory.Intertwining
  (A : Type u_1) {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) : (σ.tprod (Representation.trivial A G A)).Equiv σ
• Representation.TensorProduct.comm 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : (ρ.tprod σ).Equiv (σ.tprod ρ)
• Representation.IntertwiningMap.lTensor 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap τ) : (ρ.tprod σ).IntertwiningMap (ρ.tprod τ)
• Representation.IntertwiningMap.rTensor 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap τ) : (σ.tprod ρ).IntertwiningMap (τ.tprod ρ)
• Representation.IntertwiningMap.tensor 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} {P : Type u_6} [AddCommMonoid P] [Module A P] {π : Representation A G P} (f : ρ.IntertwiningMap σ) (g : τ.IntertwiningMap π) : (ρ.tprod τ).IntertwiningMap (σ.tprod π)
• Representation.IntertwiningMap.lTensor_id 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} : Representation.IntertwiningMap.lTensor ρ (Representation.IntertwiningMap.id σ) = Representation.IntertwiningMap.id (ρ.tprod σ)
• Representation.IntertwiningMap.rTensor_id 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} : Representation.IntertwiningMap.rTensor ρ (Representation.IntertwiningMap.id σ) = Representation.IntertwiningMap.id (σ.tprod ρ)
• Representation.TensorProduct.comm_symm 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : (Representation.TensorProduct.comm σ ρ).symm = Representation.TensorProduct.comm ρ σ
• Representation.IntertwiningMap.toLinearMap_lTensor 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f : ρ.IntertwiningMap σ) : (Representation.IntertwiningMap.lTensor τ f).toLinearMap = LinearMap.lTensor U f.toLinearMap
• Representation.IntertwiningMap.toLinearMap_rTensor 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap τ) : (Representation.IntertwiningMap.rTensor ρ f).toLinearMap = LinearMap.rTensor V f.toLinearMap
• Representation.IntertwiningMap.toLinearMap_tensor 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} {P : Type u_6} [AddCommMonoid P] [Module A P] {π : Representation A G P} (f : ρ.IntertwiningMap σ) (g : τ.IntertwiningMap π) : (f.tensor g).toLinearMap = TensorProduct.map f.toLinearMap g.toLinearMap
• Representation.TensorProduct.assoc 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) : ((ρ.tprod σ).tprod τ).Equiv (ρ.tprod (σ.tprod τ))
• Representation.IntertwiningMap.lTensor_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap τ) (v : V) (w : W) : (Representation.IntertwiningMap.lTensor ρ f) (v ⊗ₜ[A] w) = v ⊗ₜ[A] f w
• Representation.IntertwiningMap.rTensor_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f : σ.IntertwiningMap τ) (v : V) (w : W) : (Representation.IntertwiningMap.rTensor ρ f) (w ⊗ₜ[A] v) = f w ⊗ₜ[A] v
• Representation.IntertwiningMap.lTensor_comp_rTensor 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} {Q : Type u_7} [AddCommMonoid Q] [Module A Q] {υ : Representation A G Q} (f : ρ.IntertwiningMap τ) (g : σ.IntertwiningMap υ) : (Representation.IntertwiningMap.lTensor τ g).comp (Representation.IntertwiningMap.rTensor σ f) = f.tensor g
• Representation.IntertwiningMap.rTensor_comp_lTensor 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} {Q : Type u_7} [AddCommMonoid Q] [Module A Q] {υ : Representation A G Q} (f : ρ.IntertwiningMap τ) (g : σ.IntertwiningMap υ) : (Representation.IntertwiningMap.rTensor υ f).comp (Representation.IntertwiningMap.lTensor ρ g) = f.tensor g
• Representation.TensorProduct.toLinearMap_lid 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) : (↑(Representation.TensorProduct.lid A σ)).toLinearMap = ↑(TensorProduct.lid A W)
• Representation.TensorProduct.toLinearMap_rid 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) : (↑(Representation.TensorProduct.rid A σ)).toLinearMap = ↑(TensorProduct.rid A W)
• Representation.TensorProduct.toLinearMap_comm 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : (↑(Representation.TensorProduct.comm ρ σ)).toLinearMap = ↑(TensorProduct.comm A V W)
• Representation.TensorProduct.comm_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (v : V) (w : W) : (Representation.TensorProduct.comm ρ σ) (v ⊗ₜ[A] w) = w ⊗ₜ[A] v
• Representation.IntertwiningMap.tensor_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} {P : Type u_6} [AddCommMonoid P] [Module A P] {π : Representation A G P} (f : ρ.IntertwiningMap σ) (g : τ.IntertwiningMap π) (v : V) (w : U) : (f.tensor g) (v ⊗ₜ[A] w) = f v ⊗ₜ[A] g w
• Representation.TensorProduct.lid_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) (a : A) (w : W) : (Representation.TensorProduct.lid A σ) (a ⊗ₜ[A] w) = a • w
• Representation.TensorProduct.rid_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) (w : W) (a : A) : (Representation.TensorProduct.rid A σ) (w ⊗ₜ[A] a) = a • w
• Representation.IntertwiningMap.lTensor_zero 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} : Representation.IntertwiningMap.lTensor ρ 0 = 0
• Representation.IntertwiningMap.rTensor_zero 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} : Representation.IntertwiningMap.rTensor ρ 0 = 0
• Representation.TensorProduct.lid_symm_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) (w : W) : (Representation.TensorProduct.lid A σ).symm w = 1 ⊗ₜ[A] w
• Representation.TensorProduct.rid_symm_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {W : Type u_4} [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W] (σ : Representation A G W) (w : W) : (Representation.TensorProduct.rid A σ).symm w = w ⊗ₜ[A] 1
• Representation.IntertwiningMap.lTensor_smul 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (a : A) (f : σ.IntertwiningMap τ) : Representation.IntertwiningMap.lTensor ρ (a • f) = a • Representation.IntertwiningMap.lTensor ρ f
• Representation.IntertwiningMap.rTensor_smul 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (a : A) (f : σ.IntertwiningMap τ) : Representation.IntertwiningMap.rTensor ρ (a • f) = a • Representation.IntertwiningMap.rTensor ρ f
• Representation.TensorProduct.comm_comp_lTensor 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (f : σ.IntertwiningMap τ) : (↑(Representation.TensorProduct.comm ρ τ)).comp (Representation.IntertwiningMap.lTensor ρ f) = (Representation.IntertwiningMap.rTensor ρ f).comp ↑(Representation.TensorProduct.comm ρ σ)
• Representation.TensorProduct.comm_comp_rTensor 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (f : σ.IntertwiningMap τ) : (↑(Representation.TensorProduct.comm τ ρ)).comp (Representation.IntertwiningMap.rTensor ρ f) = (Representation.IntertwiningMap.lTensor ρ f).comp ↑(Representation.TensorProduct.comm σ ρ)
• Representation.IntertwiningMap.tensor_smul_left 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} {P : Type u_6} [AddCommMonoid P] [Module A P] {π : Representation A G P} (a : A) (f : ρ.IntertwiningMap σ) (g : τ.IntertwiningMap π) : (a • f).tensor g = a • f.tensor g
• Representation.IntertwiningMap.tensor_smul_right 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} {P : Type u_6} [AddCommMonoid P] [Module A P] {π : Representation A G P} (f : ρ.IntertwiningMap σ) (a : A) (g : τ.IntertwiningMap π) : f.tensor (a • g) = a • f.tensor g
• Representation.IntertwiningMap.lTensor_add 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f₁ f₂ : σ.IntertwiningMap τ) : Representation.IntertwiningMap.lTensor ρ (f₁ + f₂) = Representation.IntertwiningMap.lTensor ρ f₁ + Representation.IntertwiningMap.lTensor ρ f₂
• Representation.IntertwiningMap.rTensor_add 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} (f₁ f₂ : σ.IntertwiningMap τ) : Representation.IntertwiningMap.rTensor ρ (f₁ + f₂) = Representation.IntertwiningMap.rTensor ρ f₁ + Representation.IntertwiningMap.rTensor ρ f₂
• Representation.IntertwiningMap.tensor_add_left 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} {P : Type u_6} [AddCommMonoid P] [Module A P] {π : Representation A G P} (f₁ f₂ : ρ.IntertwiningMap σ) (g : τ.IntertwiningMap π) : (f₁ + f₂).tensor g = f₁.tensor g + f₂.tensor g
• Representation.IntertwiningMap.tensor_add_right 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] {ρ : Representation A G V} {σ : Representation A G W} {τ : Representation A G U} {P : Type u_6} [AddCommMonoid P] [Module A P] {π : Representation A G P} (f : ρ.IntertwiningMap σ) (g₁ g₂ : τ.IntertwiningMap π) : f.tensor (g₁ + g₂) = f.tensor g₁ + f.tensor g₂
• Representation.Equiv.dualTensorHom 📋 Mathlib.RepresentationTheory.Intertwining
  {G : Type u_6} {k : Type u_7} {V : Type u_8} {W : Type u_9} [Group G] [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] [FiniteDimensional k V] (ρ : Representation k G V) (σ : Representation k G W) : (ρ.dual.tprod σ).Equiv (ρ.linHom σ)
• Representation.TensorProduct.toLinearMap_assoc 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) : (↑(Representation.TensorProduct.assoc ρ σ τ)).toLinearMap = ↑(TensorProduct.assoc A V W U)
• Representation.TensorProduct.assoc_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) (v : V) (w : W) (u : U) : (Representation.TensorProduct.assoc ρ σ τ) (v ⊗ₜ[A] w ⊗ₜ[A] u) = v ⊗ₜ[A] (w ⊗ₜ[A] u)
• Representation.TensorProduct.assoc_symm_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [CommSemiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid U] [Module A V] [Module A W] [Module A U] (ρ : Representation A G V) (σ : Representation A G W) (τ : Representation A G U) : (↑(Representation.TensorProduct.assoc ρ σ τ).symm).toLinearMap = ↑(TensorProduct.assoc A V W U).symm
• Representation.Equiv.dualTensorHom_invFun 📋 Mathlib.RepresentationTheory.Intertwining
  {G : Type u_6} {k : Type u_7} {V : Type u_8} {W : Type u_9} [Group G] [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] [FiniteDimensional k V] (ρ : Representation k G V) (σ : Representation k G W) (a✝ : V →ₗ[k] W) : (Representation.Equiv.dualTensorHom ρ σ).invFun a✝ = (LinearEquiv.ofBijective (dualTensorHom k V W) ⋯).symm a✝
• Representation.Equiv.dualTensorHom_toFun 📋 Mathlib.RepresentationTheory.Intertwining
  {G : Type u_6} {k : Type u_7} {V : Type u_8} {W : Type u_9} [Group G] [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] [FiniteDimensional k V] (ρ : Representation k G V) (σ : Representation k G W) (x : TensorProduct k (Module.Dual k V) W) : (Representation.Equiv.dualTensorHom ρ σ) x = (dualTensorHom k V W) x
• Representation.LinearizeMonoidal.δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).IntertwiningMap ((Representation.linearize k G X).tprod (Representation.linearize k G Y))
• Representation.LinearizeMonoidal.μ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : ((Representation.linearize k G X).tprod (Representation.linearize k G Y)).IntertwiningMap (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
• 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)
• Representation.LinearizeMonoidal.μ_δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : (Representation.LinearizeMonoidal.μ X Y).comp (Representation.LinearizeMonoidal.δ X Y) = Representation.IntertwiningMap.id (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
• Representation.LinearizeMonoidal.μ_apply_single_single 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (x : X.V) (y : Y.V) (r s : k) : (Representation.LinearizeMonoidal.μ X Y) (MonoidAlgebra.single x r ⊗ₜ[k] MonoidAlgebra.single y s) = MonoidAlgebra.single (x, y) (r * s)
• Representation.LinearizeMonoidal.δ_apply_single 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (xy : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V) : (Representation.LinearizeMonoidal.δ X Y) (MonoidAlgebra.single xy 1) = MonoidAlgebra.single xy.1 1 ⊗ₜ[k] MonoidAlgebra.single xy.2 1
• Representation.LinearizeMonoidal.coeff_μ_tmul 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (l1 : MonoidAlgebra k X.V) (l2 : MonoidAlgebra k Y.V) (xy : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).V) : ((Representation.LinearizeMonoidal.μ X Y) (l1 ⊗ₜ[k] l2)).coeff xy = l1.coeff xy.1 * l2.coeff xy.2
• Representation.LinearizeMonoidal.δ_μ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y : Action (Type w) G) {k : Type u} [CommSemiring k] : (Representation.LinearizeMonoidal.δ X Y).comp (Representation.LinearizeMonoidal.μ X Y) = Representation.IntertwiningMap.id ((Representation.linearize k G X).tprod (Representation.linearize k G Y))
• Representation.LinearizeMonoidal.lTensor_comp_δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} (Z : Action (Type w) G) {k : Type u} [CommSemiring k] (f : X ⟶ Y) : (Representation.IntertwiningMap.lTensor (Representation.linearize k G Z) (Representation.linearizeMap f)).comp (Representation.LinearizeMonoidal.δ Z X) = (Representation.LinearizeMonoidal.δ Z Y).comp (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f))
• Representation.LinearizeMonoidal.rTensor_comp_δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} (Z : Action (Type w) G) {k : Type u} [CommSemiring k] (f : X ⟶ Y) : (Representation.IntertwiningMap.rTensor (Representation.linearize k G Z) (Representation.linearizeMap f)).comp (Representation.LinearizeMonoidal.δ X Z) = (Representation.LinearizeMonoidal.δ Y Z).comp (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z))
• Representation.LinearizeMonoidal.μ_comp_lTensor 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (f : X ⟶ Y) (Z : Action (Type w) G) : (Representation.LinearizeMonoidal.μ Z Y).comp (Representation.IntertwiningMap.lTensor (Representation.linearize k G Z) (Representation.linearizeMap f)) = (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)).comp (Representation.LinearizeMonoidal.μ Z X)
• Representation.LinearizeMonoidal.μ_comp_rTensor 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {X Y : Action (Type w) G} {k : Type u} [CommSemiring k] (f : X ⟶ Y) (Z : Action (Type w) G) : (Representation.LinearizeMonoidal.μ Y Z).comp (Representation.IntertwiningMap.rTensor (Representation.linearize k G Z) (Representation.linearizeMap f)) = (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)).comp (Representation.LinearizeMonoidal.μ X Z)
• Representation.LinearizeMonoidal.μ_leftUnitor 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X : Action (Type w) G) {k : Type u} [CommSemiring k] : ↑(Representation.TensorProduct.lid k (Representation.linearize k G X)) = ((Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom).comp (Representation.LinearizeMonoidal.μ (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type w) G)) X)).comp (Representation.IntertwiningMap.rTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.ε k G))
• Representation.LinearizeMonoidal.μ_rightUnitor 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X : Action (Type w) G) {k : Type u} [CommSemiring k] : ↑(Representation.TensorProduct.rid k (Representation.linearize k G X)) = ((Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom).comp (Representation.LinearizeMonoidal.μ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type w) G)))).comp (Representation.IntertwiningMap.lTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.ε k G))
• Representation.LinearizeMonoidal.leftUnitor_δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {k : Type u} [CommSemiring k] (X : Action (Type u) G) : ↑(Representation.TensorProduct.lid k (Representation.linearize k G X)).symm = ((Representation.IntertwiningMap.rTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.η k G)).comp (Representation.LinearizeMonoidal.δ (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G)) X)).comp (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv)
• Representation.LinearizeMonoidal.rightUnitor_δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] {k : Type u} [CommSemiring k] (X : Action (Type u) G) : ↑(Representation.TensorProduct.rid k (Representation.linearize k G X)).symm = ((Representation.IntertwiningMap.lTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.η k G)).comp (Representation.LinearizeMonoidal.δ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G)))).comp (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)
• Representation.LinearizeMonoidal.μ_comp_assoc 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y Z : Action (Type w) G) {k : Type u} [CommSemiring k] : ((Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom).comp (Representation.LinearizeMonoidal.μ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)).comp (Representation.IntertwiningMap.rTensor (Representation.linearize k G Z) (Representation.LinearizeMonoidal.μ X Y)) = ((Representation.LinearizeMonoidal.μ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).comp (Representation.IntertwiningMap.lTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.μ Y Z))).comp ↑(Representation.TensorProduct.assoc (Representation.linearize k G X) (Representation.linearize k G Y) (Representation.linearize k G Z))
• Representation.LinearizeMonoidal.assoc_comp_δ 📋 Mathlib.RepresentationTheory.Action
  {G : Type v} [Monoid G] (X Y Z : Action (Type w) G) {k : Type u} [CommSemiring k] : ((↑(Representation.TensorProduct.assoc (Representation.linearize k G X) (Representation.linearize k G Y) (Representation.linearize k G Z))).comp (Representation.IntertwiningMap.rTensor (Representation.linearize k G Z) (Representation.LinearizeMonoidal.δ X Y))).comp (Representation.LinearizeMonoidal.δ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) = ((Representation.IntertwiningMap.lTensor (Representation.linearize k G X) (Representation.LinearizeMonoidal.δ Y Z)).comp (Representation.LinearizeMonoidal.δ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))).comp (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
• Representation.finsuppTensorLeft 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) (α : Type w') [DecidableEq α] : ((σ.finsupp α).tprod ρ).Equiv ((σ.tprod ρ).finsupp α)
• Representation.finsuppTensorRight 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) (α : Type w') [DecidableEq α] : (σ.tprod (ρ.finsupp α)).Equiv ((σ.tprod ρ).finsupp α)
• Representation.leftRegularTensorTrivialIsoFree 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {k : Type u} [CommSemiring k] (α : Type w') : ((Representation.leftRegular k G).tprod (Representation.trivial k G (MonoidAlgebra k α))).Equiv (Representation.free k G α)
• Representation.finsuppTensorLeft_apply_tmul 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) {α : Type w'} [DecidableEq α] (f : α →₀ V) (w : W) : (σ.finsuppTensorLeft ρ α) (f ⊗ₜ[k] w) = f.sum fun i v => fun₀ | i => v ⊗ₜ[k] w
• Representation.finsuppTensorRight_apply_tmul 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) {α : Type w'} [DecidableEq α] (v : V) (f : α →₀ W) : (σ.finsuppTensorRight ρ α) (v ⊗ₜ[k] f) = f.sum fun i w => fun₀ | i => v ⊗ₜ[k] w
• Representation.finsuppTensorLeft_apply_tmul_apply 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) {α : Type w'} [DecidableEq α] (f : α →₀ V) (w : W) (i : α) : ((σ.finsuppTensorLeft ρ α) (f ⊗ₜ[k] w)) i = f i ⊗ₜ[k] w
• Representation.finsuppTensorRight_apply_tmul_apply 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) {α : Type w'} [DecidableEq α] (v : V) (f : α →₀ W) (i : α) : ((σ.finsuppTensorRight ρ α) (v ⊗ₜ[k] f)) i = v ⊗ₜ[k] f i
• Representation.leftRegularTensorTrivialIsoFree_apply_single_tmul_single 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {k : Type u} [CommSemiring k] {α : Type w'} (g : G) (i : α) (r s : k) : (Representation.leftRegularTensorTrivialIsoFree α) (MonoidAlgebra.single g r ⊗ₜ[k] MonoidAlgebra.single i s) = fun₀ | i => MonoidAlgebra.single g (r * s)
• Representation.finsuppTensorLeft_symm_apply_single 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) {α : Type w'} [DecidableEq α] (i : α) (v : V) (w : W) : ((σ.finsuppTensorLeft ρ α).symm fun₀ | i => v ⊗ₜ[k] w) = (fun₀ | i => v) ⊗ₜ[k] w
• Representation.finsuppTensorRight_symm_apply_single 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {W : Type w'} [AddCommMonoid W] {k : Type u} [CommSemiring k] [Module k V] [Module k W] (σ : Representation k G V) (ρ : Representation k G W) {α : Type w'} [DecidableEq α] (i : α) (v : V) (w : W) : ((σ.finsuppTensorRight ρ α).symm fun₀ | i => v ⊗ₜ[k] w) = v ⊗ₜ[k] fun₀ | i => w
• Representation.leftRegularTensorTrivialIsoFree_symm_apply_single_single 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {k : Type u} [CommSemiring k] {α : Type w'} (i : α) (g : G) (r : k) : ((Representation.leftRegularTensorTrivialIsoFree α).symm fun₀ | i => MonoidAlgebra.single g r) = MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single i r
• Rep.of_tensor 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] (σ : Representation k G X) (ρ : Representation k G Y) : Rep.of (σ.tprod ρ) = CategoryTheory.MonoidalCategoryStruct.tensorObj (Rep.of σ) (Rep.of ρ)
• Rep.tensor_ρ 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Rep.{u, u, v} k G} : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).ρ = X.ρ.tprod Y.ρ
• Rep.hom_hom_leftUnitor 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X : Rep.{u, u, v} k G} : Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom = ↑(Representation.TensorProduct.lid k X.ρ)
• Rep.hom_hom_rightUnitor 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X : Rep.{u, u, v} k G} : Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom = ↑(Representation.TensorProduct.rid k X.ρ)
• Rep.hom_inv_leftUnitor 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X : Rep.{u, u, v} k G} : Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv = ↑(Representation.TensorProduct.lid k X.ρ).symm
• Rep.hom_inv_rightUnitor 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X : Rep.{u, u, v} k G} : Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv = ↑(Representation.TensorProduct.rid k X.ρ).symm
• Rep.hom_braiding 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Rep.{u, u, v} k G} : Rep.Hom.hom (β_ X Y).hom = ↑(Representation.TensorProduct.comm X.ρ Y.ρ)
• Rep.δ_def 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Action (Type u) G} : CategoryTheory.Functor.OplaxMonoidal.δ (Rep.linearization k G) X Y = Rep.ofHom (Representation.LinearizeMonoidal.δ X Y)
• Rep.μ_def 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y : Action (Type u) G} : CategoryTheory.Functor.LaxMonoidal.μ (Rep.linearization k G) X Y = Rep.ofHom (Representation.LinearizeMonoidal.μ X Y)
• Rep.hom_hom_associator 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y Z : Rep.{u, u, v} k G} : Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom = ↑(Representation.TensorProduct.assoc X.ρ Y.ρ Z.ρ)
• Rep.hom_inv_associator 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [CommRing k] [Monoid G] {X Y Z : Rep.{u, u, v} k G} : Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv = ↑(Representation.TensorProduct.assoc X.ρ Y.ρ Z.ρ).symm
• Rep.tensorHomEquiv_symm_apply 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} [CommRing k] {G : Type v} [Group G] (A B C : Rep.{u, u, v} k G) (f : B ⟶ A.ihom.obj C) : (A.tensorHomEquiv B C).symm f = Rep.ofHom { toLinearMap := (TensorProduct.uncurry (RingHom.id k) ↑A ↑B ↑C) (Rep.Hom.hom f).flip, isIntertwining' := ⋯ }
• Representation.char_tensor 📋 Mathlib.RepresentationTheory.Character
  {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [AddCommGroup W] [Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W) : (ρ.tprod σ).character = ρ.character * σ.character
• Representation.ofCoinvariantsTprodLeftRegular 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : (ρ.tprod (Representation.leftRegular k G)).Coinvariants →ₗ[k] V
• Representation.coinvariantsTprodLeftRegularLEquiv 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : (ρ.tprod (Representation.leftRegular k G)).Coinvariants ≃ₗ[k] V
• Representation.Coinvariants.mk_inv_tmul 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} {W : Type u_9} [CommRing k] [Group G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (ρ : Representation k G V) (τ : Representation k G W) (x : V) (y : W) (g : G) : (Representation.Coinvariants.mk (ρ.tprod τ)) ((ρ g⁻¹) x ⊗ₜ[k] y) = (Representation.Coinvariants.mk (ρ.tprod τ)) (x ⊗ₜ[k] (τ g) y)
• Representation.Coinvariants.mk_tmul_inv 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} {W : Type u_9} [CommRing k] [Group G] [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W] (ρ : Representation k G V) (τ : Representation k G W) (x : V) (y : W) (g : G) : (Representation.Coinvariants.mk (ρ.tprod τ)) (x ⊗ₜ[k] (τ g⁻¹) y) = (Representation.Coinvariants.mk (ρ.tprod τ)) ((ρ g) x ⊗ₜ[k] y)
• Rep.finsuppToCoinvariantsTensorFree 📋 Mathlib.RepresentationTheory.Coinvariants
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (α : Type u) [DecidableEq α] : (α →₀ ↑A) →ₗ[k] (A.ρ.tprod (Rep.free k G α).ρ).Coinvariants
• Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (x : V) (g : G) (r : k) : ρ.ofCoinvariantsTprodLeftRegular ((Representation.Coinvariants.mk (ρ.tprod (Representation.leftRegular k G))) (x ⊗ₜ[k] MonoidAlgebra.single g r)) = r • (ρ g⁻¹) x
• Representation.coinvariantsTprodLeftRegularLEquiv_apply 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (x : (ρ.tprod (Representation.leftRegular k G)).Coinvariants) : ρ.coinvariantsTprodLeftRegularLEquiv x = ρ.ofCoinvariantsTprodLeftRegular x
• Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (a : V) : ρ.coinvariantsTprodLeftRegularLEquiv.symm a = (Representation.Coinvariants.mk (ρ.tprod (Representation.leftRegular k G))) (a ⊗ₜ[k] MonoidAlgebra.single 1 1)
• Rep.coinvariantsTensorFreeLEquiv_apply 📋 Mathlib.RepresentationTheory.Coinvariants
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (α : Type u) [DecidableEq α] (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj A (Rep.free k G α)).ρ.Coinvariants) : (A.coinvariantsTensorFreeToFinsupp α) x = (A.coinvariantsTensorFreeToFinsupp α) x
• Rep.coinvariantsTensorFreeLEquiv_symm_apply 📋 Mathlib.RepresentationTheory.Coinvariants
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (α : Type u) [DecidableEq α] (a : α →₀ ↑A) : (A.coinvariantsTensorFreeLEquiv α).symm a = (A.finsuppToCoinvariantsTensorFree α) a
• Rep.finsuppToCoinvariantsTensorFree_single 📋 Mathlib.RepresentationTheory.Coinvariants
  {k G : Type u} [CommRing k] [Group G] {A : Rep.{u, u, u} k G} {α : Type u} [DecidableEq α] (i : α) (x : ↑A) : ((A.finsuppToCoinvariantsTensorFree α) fun₀ | i => x) = (Representation.Coinvariants.mk (A.ρ.tprod (Representation.free k G α))) (x ⊗ₜ[k] fun₀ | i => MonoidAlgebra.single 1 1)
• Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single 📋 Mathlib.RepresentationTheory.Coinvariants
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) {α : Type u} [DecidableEq α] (x : ↑A) (i : α) (g : G) (r : k) : (A.coinvariantsTensorFreeToFinsupp α) ((Representation.Coinvariants.mk (A.ρ.tprod (Representation.free k G α))) (x ⊗ₜ[k] fun₀ | i => MonoidAlgebra.single g r)) = fun₀ | i => r • (A.ρ g⁻¹) x
• Representation.ind 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) : Representation k H (Representation.IndV φ ρ)
• Representation.IndV.mk 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) (h : H) : A →ₗ[k] Representation.IndV φ ρ
• Representation.IndV.hom_ext 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} {B : Type u_5} [AddCommGroup A] [Module k A] (ρ : Representation k G A) [AddCommGroup B] [Module k B] {f g : Representation.IndV φ ρ →ₗ[k] B} (hfg : ∀ (h : H), f ∘ₗ Representation.IndV.mk φ ρ h = g ∘ₗ Representation.IndV.mk φ ρ h) : f = g
• Representation.IndV.hom_ext_iff 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] {φ : G →* H} {A : Type u_4} {B : Type u_5} [AddCommGroup A] [Module k A] {ρ : Representation k G A} [AddCommGroup B] [Module k B] {f g : Representation.IndV φ ρ →ₗ[k] B} : f = g ↔ ∀ (h : H), f ∘ₗ Representation.IndV.mk φ ρ h = g ∘ₗ Representation.IndV.mk φ ρ h
• Rep.indResHomEquiv_symm_apply 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u} {G : Type v} {H : Type v'} [CommRing k] [Group G] [Group H] (φ : G →* H) (A : Rep.{max w v' u, u, v} k G) (B : Rep.{max w v' u, u, v'} k H) (f : A ⟶ Rep.res φ B) : (Rep.indResHomEquiv φ A B).symm f = Rep.ofHom { toLinearMap := Representation.Coinvariants.lift (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ) (TensorProduct.lift (((Finsupp.lift (↑A →ₗ[k] ↑B) k H) fun h => B.ρ h⁻¹ ∘ₗ (Rep.Hom.hom f).toLinearMap) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k))) ⋯, isIntertwining' := ⋯ }
• Rep.coinvariantsTensorIndInv_mk_tmul_indMk 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u} [CommRing k] {G H : Type u} [Group G] [Group H] (φ : G →* H) {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (x : ↑A) (y : ↑B) : (CategoryTheory.ConcreteCategory.hom (Rep.coinvariantsTensorIndInv φ A B)) ((Representation.Coinvariants.mk (A.ρ.tprod (Rep.res φ B).ρ)) (x ⊗ₜ[k] y)) = (((Rep.ind φ A).coinvariantsTensorMk B) ((Representation.IndV.mk φ A.ρ 1) x)) y
• Representation.ind_mk 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) (h₁ h₂ : H) (a : A) : ((Representation.ind φ ρ) h₁) ((Representation.IndV.mk φ ρ h₂) a) = (Representation.IndV.mk φ ρ (h₂ * h₁⁻¹)) a
• Rep.coinvariantsTensorIndHom_mk_tmul_indVMk 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u} [CommRing k] {G H : Type u} [Group G] [Group H] (φ : G →* H) {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (h : H) (x : ↑A) (y : ↑B) : (CategoryTheory.ConcreteCategory.hom (Rep.coinvariantsTensorIndHom φ A B)) ((((Rep.ind φ A).coinvariantsTensorMk B) ((Representation.IndV.mk φ A.ρ h) x)) y) = ((A.coinvariantsTensorMk (Rep.res φ B)) x) ((B.ρ h) y)
• Representation.ind_apply 📋 Mathlib.RepresentationTheory.Induced
  {k : Type u_1} {G : Type u_2} {H : Type u_3} [CommRing k] [Group G] [Group H] (φ : G →* H) {A : Type u_4} [AddCommGroup A] [Module k A] (ρ : Representation k G A) (h : H) : (Representation.ind φ ρ) h = Representation.Coinvariants.map (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) ρ) (Representation.tprod (MonoidHom.comp (Representation.leftRegular k H) φ) ρ) { toLinearMap := LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x => x * h⁻¹), isIntertwining' := ⋯ }
• Rep.coindToInd 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} (A : Rep.{w, u, v} k ↥S) [S.FiniteIndex] : ↑(Rep.coind.{u, v, v, w} S.subtype A) →ₗ[k] ↑(Rep.ind S.subtype A)
• Rep.indToCoind 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep.{w, u, v} k ↥S) : ↑(Rep.ind S.subtype A) →ₗ[k] ↑(Rep.coind.{u, v, v, w} S.subtype A)
• Rep.coindToInd_indToCoind 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep.{w, u, v} k ↥S) [S.FiniteIndex] : A.indToCoind ∘ₗ A.coindToInd = LinearMap.id
• Rep.indToCoind_coindToInd 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep.{w, u, v} k ↥S) [S.FiniteIndex] : A.coindToInd ∘ₗ A.indToCoind = LinearMap.id
• Rep.coindToInd_of_support_subset_orbit 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} {A : Rep.{w, u, v} k ↥S} [S.FiniteIndex] (g : G) (f : ↑(Rep.coind.{u, v, v, w} S.subtype A)) (hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g) : A.coindToInd f = (Representation.IndV.mk S.subtype A.ρ g) (↑f g)
• Rep.coindToInd_apply 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} (A : Rep.{w, u, v} k ↥S) [S.FiniteIndex] (f : ↑(Rep.coind.{u, v, v, w} S.subtype A)) : A.coindToInd f = ∑ g, g.liftOn (fun g => (Representation.IndV.mk S.subtype A.ρ g) (↑f g)) ⋯
• Rep.indCoindIso_hom_hom_toLinearMap 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (A : Rep.{max w u, u, v} k ↥S) : (Rep.Hom.hom A.indCoindIso.hom).toLinearMap = A.indToCoind
• Rep.indCoindIso_inv_hom_toLinearMap 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (A : Rep.{max w u, u, v} k ↥S) : (Rep.Hom.hom A.indCoindIso.inv).toLinearMap = { toFun := (Representation.Equiv.mk (LinearEquiv.ofLinearMap A.indToCoind A.coindToInd ⋯ ⋯) ⋯).invFun, map_add' := ⋯, map_smul' := ⋯ }
• Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
  {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (a : ↑A) : (ModuleCat.Hom.hom ((Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso A g hg).inv.f i)) a = ((↑A.ρ.coinvariantsTprodLeftRegularLEquiv).inverse ⇑A.ρ.coinvariantsTprodLeftRegularLEquiv.symm ⋯ ⋯) a
• Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
  {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (a✝ : TensorProduct k (↑A) (MonoidAlgebra k G) ⧸ (Representation.Coinvariants.ker (A.ρ.tprod (Representation.leftRegular k G))).toAddSubgroup) : (ModuleCat.Hom.hom ((Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso A g hg).hom.f i)) a✝ = (QuotientAddGroup.lift (Representation.Coinvariants.ker (A.ρ.tprod (Representation.leftRegular k G))).toAddSubgroup (TensorProduct.lift ((Finsupp.linearCombination k fun g => A.ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ ↑(TensorProduct.comm k (↑A) (MonoidAlgebra k G))).toAddMonoidHom ⋯) a✝

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 ce5dd8c