Loogle!

Result

Found 337 declarations mentioning Representation.IntertwiningMap. Of these, only the first 200 are shown.

• Representation.IntertwiningMap.id 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : ρ.IntertwiningMap ρ
• Representation.IntertwiningMap 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Type (max u_3 u_4)
• Representation.IntertwiningMap.instMonoid 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : Monoid (ρ.IntertwiningMap ρ)
• Representation.IntertwiningMap.instMul 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : Mul (ρ.IntertwiningMap ρ)
• Representation.IntertwiningMap.instNatCast 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : NatCast (ρ.IntertwiningMap ρ)
• Representation.IntertwiningMap.instOne 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : One (ρ.IntertwiningMap ρ)
• Representation.IntertwiningMap.instSemigroup 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : Semigroup (ρ.IntertwiningMap ρ)
• Representation.IntertwiningMap.instSemiring 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : Semiring (ρ.IntertwiningMap ρ)
• Representation.IntertwiningMap.instPowNat 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : Pow (ρ.IntertwiningMap ρ) ℕ
• Representation.IntertwiningMap.instAdd 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Add (ρ.IntertwiningMap σ)
• Representation.IntertwiningMap.instAddCommMonoid 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : AddCommMonoid (ρ.IntertwiningMap σ)
• Representation.IntertwiningMap.instZero 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Zero (ρ.IntertwiningMap σ)
• Representation.IntertwiningMap.instAlgebra 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : Algebra A (ρ.IntertwiningMap ρ)
• Representation.IntertwiningMap.instSMulNat 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : SMul ℕ (ρ.IntertwiningMap σ)
• Representation.IntertwiningMap.instFunLike 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : FunLike (ρ.IntertwiningMap σ) V W
• Representation.IntertwiningMap.instAddCommGroup 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : AddCommGroup (ρ.IntertwiningMap σ)
• Representation.IntertwiningMap.instNeg 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Neg (ρ.IntertwiningMap σ)
• Representation.IntertwiningMap.instSub 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Sub (ρ.IntertwiningMap σ)
• Representation.IntertwiningMap.instSMulInt 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : SMul ℤ (ρ.IntertwiningMap σ)
• Representation.IntertwiningMap.ker 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) : Subrepresentation ρ
• Representation.IntertwiningMap.range 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) : Subrepresentation σ
• Representation.IntertwiningMap.instSMul 📋 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) : SMul A (ρ.IntertwiningMap σ)
• Representation.Equiv.toIntertwiningMap 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (self : ρ.Equiv σ) : ρ.IntertwiningMap σ
• Representation.IntertwiningMap.coe_id 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : ⇑(Representation.IntertwiningMap.id ρ) = id
• Representation.IntertwiningMap.id_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (v : V) : (Representation.IntertwiningMap.id ρ) v = v
• Representation.Equiv.toIntertwiningMap_refl 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring A] [Monoid G] [AddCommMonoid V] [Module A V] {ρ : Representation A G V} : ↑(Representation.Equiv.refl ρ) = Representation.IntertwiningMap.id ρ
• Representation.IntertwiningMap.centralMul 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (g : G) (hg : g ∈ Submonoid.center G) : ρ.IntertwiningMap ρ
• Representation.IntertwiningMap.toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (self : ρ.IntertwiningMap σ) : V →ₗ[A] W
• Representation.IntertwiningMap.instLinearMapClass 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : LinearMapClass (ρ.IntertwiningMap σ) A V W
• Representation.IntertwiningMap.fst 📋 Mathlib.RepresentationTheory.Intertwining
  (A : Type u_1) {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : (ρ.prod σ).IntertwiningMap ρ
• Representation.IntertwiningMap.inl 📋 Mathlib.RepresentationTheory.Intertwining
  (A : Type u_1) {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : ρ.IntertwiningMap (ρ.prod σ)
• Representation.IntertwiningMap.inr 📋 Mathlib.RepresentationTheory.Intertwining
  (A : Type u_1) {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : σ.IntertwiningMap (ρ.prod σ)
• Representation.IntertwiningMap.snd 📋 Mathlib.RepresentationTheory.Intertwining
  (A : Type u_1) {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : (ρ.prod σ).IntertwiningMap σ
• Representation.IntertwiningMap.instModule 📋 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) : Module A (ρ.IntertwiningMap σ)
• Representation.IntertwiningMap.comp 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring 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 τ) (g : ρ.IntertwiningMap σ) : ρ.IntertwiningMap τ
• Representation.IntertwiningMap.toLinearMap_injective 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Function.Injective fun f => f.toLinearMap
• Representation.IntertwiningMap.coe_one 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : ⇑1 = id
• Representation.IntertwiningMap.ker_toSubmodule 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) : (Representation.IntertwiningMap.ker ρ σ f).toSubmodule = f.ker
• Representation.IntertwiningMap.ofBijective 📋 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} (f : ρ.IntertwiningMap σ) (hf : Function.Bijective ⇑f) : ρ.Equiv σ
• Representation.IntertwiningMap.range_toSubmodule 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) : (Representation.IntertwiningMap.range ρ σ f).toSubmodule = f.range
• Representation.IntertwiningMap.toFun_injective 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Function.Injective fun f => f.toFun
• Representation.IntertwiningMap.prod 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring 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 σ) (g : ρ.IntertwiningMap τ) : ρ.IntertwiningMap (σ.prod τ)
• Representation.IntertwiningMap.coeFnAddMonoidHom 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : ρ.IntertwiningMap σ →+ V → W
• Representation.IntertwiningMap.ext 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} {f g : ρ.IntertwiningMap σ} (h : f.toLinearMap = g.toLinearMap) : f = g
• Representation.IntertwiningMap.ext_iff 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} {f g : ρ.IntertwiningMap σ} : f = g ↔ f.toLinearMap = g.toLinearMap
• Representation.IntertwiningMap.fst_comp_inl 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} : (Representation.IntertwiningMap.fst A ρ σ).comp (Representation.IntertwiningMap.inl A ρ σ) = Representation.IntertwiningMap.id ρ
• Representation.IntertwiningMap.snd_comp_inr 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} : (Representation.IntertwiningMap.snd A ρ σ).comp (Representation.IntertwiningMap.inr A ρ σ) = Representation.IntertwiningMap.id σ
• Representation.IntertwiningMap.coe_zero 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : ⇑0 = 0
• Representation.IntertwiningMap.coe_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) : ⇑f.toLinearMap = ⇑f
• Representation.IntertwiningMap.mem_range 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (w : W) : w ∈ Representation.IntertwiningMap.range ρ σ f ↔ ∃ v, f v = w
• Representation.IntertwiningMap.toLinearMap_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (v : V) : f.toLinearMap v = f v
• Representation.IntertwiningMap.coe_eq_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) {f : ρ.IntertwiningMap σ} : ↑f = f.toLinearMap
• Representation.IntertwiningMap.fst_surjective 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Function.Surjective ⇑(Representation.IntertwiningMap.fst A ρ σ)
• Representation.IntertwiningMap.snd_surjective 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Function.Surjective ⇑(Representation.IntertwiningMap.snd A ρ σ)
• Representation.Equiv.coe_toIntertwiningMap 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) : ⇑↑φ = ⇑φ
• Representation.IntertwiningMap.coe_fst 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : ⇑(Representation.IntertwiningMap.fst A ρ σ) = Prod.fst
• Representation.IntertwiningMap.coe_snd 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : ⇑(Representation.IntertwiningMap.snd A ρ σ) = Prod.snd
• Representation.IntertwiningMap.fst_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (v : V × W) : (Representation.IntertwiningMap.fst A ρ σ) v = v.1
• Representation.IntertwiningMap.mem_ker 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (v : V) : v ∈ Representation.IntertwiningMap.ker ρ σ f ↔ f v = 0
• Representation.IntertwiningMap.snd_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (v : V × W) : (Representation.IntertwiningMap.snd A ρ σ) v = v.2
• Representation.IntertwiningMap.instFiniteOfIsNoetherian 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_6} {G : Type u_7} {V : Type u_8} {W : Type u_9} [CommRing A] [Monoid G] [AddCommGroup V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) [Module.Finite A V] [IsNoetherian A W] : Module.Finite A (ρ.IntertwiningMap σ)
• Representation.IntertwiningMap.sum_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) {ι : Type u_6} (s : Finset ι) (f : ι → ρ.IntertwiningMap σ) (v : V) : (∑ i ∈ s, f i) v = ∑ i ∈ s, (f i) v
• Representation.IntertwiningMap.zero_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) : Representation.IntertwiningMap.toLinearMap 0 = 0
• Representation.IntertwiningMap.fst_comp_inr 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} : (Representation.IntertwiningMap.fst A ρ σ).comp (Representation.IntertwiningMap.inr A ρ σ) = 0
• Representation.IntertwiningMap.snd_comp_inl 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} : (Representation.IntertwiningMap.snd A ρ σ).comp (Representation.IntertwiningMap.inl A ρ σ) = 0
• 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.toLinearMap_sum 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) {ι : Type u_6} (s : Finset ι) (f : ι → ρ.IntertwiningMap σ) : (∑ i ∈ s, f i).toLinearMap = ∑ i ∈ s, (f i).toLinearMap
• Representation.IntertwiningMap.fst_prod 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring 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 σ) (g : ρ.IntertwiningMap τ) : (Representation.IntertwiningMap.fst A σ τ).comp (f.prod g) = f
• Representation.IntertwiningMap.snd_prod 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring 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 σ) (g : ρ.IntertwiningMap τ) : (Representation.IntertwiningMap.snd A σ τ).comp (f.prod g) = g
• Representation.Equiv.toIntertwiningMap_trans 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring 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} (φ : ρ.Equiv σ) (ψ : σ.Equiv τ) : ↑(φ.trans ψ) = (↑ψ).comp ↑φ
• Representation.Equiv.mk' 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (toIntertwiningMap : ρ.IntertwiningMap σ) (invFun : W → V) (left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun := by intro; first | rfl | ext <;> rfl) (right_inv : Function.RightInverse invFun toIntertwiningMap.toFun := by intro; first | rfl | ext <;> rfl) : ρ.Equiv σ
• Representation.IntertwiningMap.centralAlgebraMul 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) {z : MonoidAlgebra A G} (hz : z ∈ Submonoid.center (MonoidAlgebra A G)) : ρ.IntertwiningMap ρ
• Representation.IntertwiningMap.coe_neg 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) : ⇑(-f) = -⇑f
• Representation.IntertwiningMap.comp_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring 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 τ) (g : ρ.IntertwiningMap σ) (v : V) : (f.comp g) v = f (g v)
• Representation.IntertwiningMap.comp_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring 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 τ) (g : ρ.IntertwiningMap σ) : (f.comp g).toLinearMap = f.toLinearMap ∘ₗ g.toLinearMap
• Representation.IntertwiningMap.coe_nsmul 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (n : ℕ) : ⇑(n • f) = n • ⇑f
• Representation.IntertwiningMap.toLinearMapl 📋 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) : ρ.IntertwiningMap σ →ₗ[A] V →ₗ[A] W
• Representation.Equiv.toLinearEquiv_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ) (v : V) : φ.toLinearEquiv v = ↑φ v
• 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.coe_ofBijective 📋 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) (f : ρ.IntertwiningMap σ) (hf : Function.Bijective ⇑f) : ⇑(f.ofBijective hf) = ⇑f
• 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.IntertwiningMap.coe_zsmul 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (z : ℤ) : ⇑(z • f) = z • ⇑f
• Representation.IntertwiningMap.mul_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (f g : ρ.IntertwiningMap ρ) (v : V) : (f * g) v = f (g v)
• Representation.IntertwiningMap.smul_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) (a : A) (f : ρ.IntertwiningMap σ) (v : V) : (a • f) v = a • f v
• Representation.IntertwiningMap.coe_add 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f g : ρ.IntertwiningMap σ) : ⇑(f + g) = ⇑f + ⇑g
• Representation.IntertwiningMap.coe_smul 📋 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) (a : A) (f : ρ.IntertwiningMap σ) : ⇑(a • f) = a • ⇑f
• Representation.IntertwiningMap.prod_comp 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring 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} (X : Type u_6) [AddCommMonoid X] [Module A X] {π : Representation A G X} (f : ρ.IntertwiningMap σ) (g₁ : σ.IntertwiningMap τ) (g₂ : σ.IntertwiningMap π) : (g₁.prod g₂).comp f = (g₁.comp f).prod (g₂.comp f)
• Representation.IntertwiningMap.add_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f g : ρ.IntertwiningMap σ) : (f + g).toLinearMap = f.toLinearMap + g.toLinearMap
• Representation.IntertwiningMap.coe_sub 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f g : ρ.IntertwiningMap σ) : ⇑(f - g) = ⇑f - ⇑g
• Representation.IntertwiningMap.comp_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 τ) (g : ρ.IntertwiningMap σ) : f.comp (a • g) = a • f.comp g
• Representation.IntertwiningMap.smul_comp 📋 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 τ) (g : ρ.IntertwiningMap σ) : (a • f).comp g = a • f.comp g
• 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.algebraMap_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (a : A) : (algebraMap A (ρ.IntertwiningMap ρ)) a = a • 1
• Representation.IntertwiningMap.coe_mul 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (f g : ρ.IntertwiningMap ρ) : (f * g).toLinearMap = f.toLinearMap * g.toLinearMap
• Representation.IntertwiningMap.add_comp 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring 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 τ) (g₁ g₂ : ρ.IntertwiningMap σ) : f.comp (g₁ + g₂) = f.comp g₁ + f.comp g₂
• Representation.IntertwiningMap.comp_add 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring 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 τ) (g : ρ.IntertwiningMap σ) : (f₁ + f₂).comp g = f₁.comp g + f₂.comp g
• Representation.IntertwiningMap.sub_toLinearMap 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} [Semiring A] [Monoid G] {V : Type u_6} {W : Type u_7} [AddCommMonoid V] [AddCommGroup W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f g : ρ.IntertwiningMap σ) : (f - g).toLinearMap = f.toLinearMap - g.toLinearMap
• Representation.IntertwiningMap.toLinearMap_smul 📋 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) (a : A) (f : ρ.IntertwiningMap σ) : (a • f).toLinearMap = a • f.toLinearMap
• Representation.IntertwiningMap.equivAlgEnd 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : ρ.IntertwiningMap ρ ≃ₐ[A] Module.End (MonoidAlgebra A G) ρ.asModule
• 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.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.mk 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (toLinearMap : V →ₗ[A] W) (isIntertwining' : ∀ (g : G), toLinearMap ∘ₗ ρ g = σ g ∘ₗ toLinearMap) : ρ.IntertwiningMap σ
• 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.IntertwiningMap.isIntertwining' 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (self : ρ.IntertwiningMap σ) (g : G) : self.toLinearMap ∘ₗ ρ g = σ g ∘ₗ self.toLinearMap
• Representation.IntertwiningMap.isIntertwining 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (g : G) (v : V) : f ((ρ g) v) = (σ g) (f v)
• Representation.IntertwiningMap.centralAlgebraMulHom 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) : ↥(Submonoid.center (MonoidAlgebra A G)) →* ρ.IntertwiningMap ρ
• LinearMap.intertwiningMap_of_isIntertwiningMap 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W) (hf : ∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)) : ρ.IntertwiningMap σ
• 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.IntertwiningMap.coe_mk 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W) (h : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f) : ⇑{ toLinearMap := f, isIntertwining' := h } = ⇑f
• Representation.IntertwiningMap.toLinearMapl_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) (self : ρ.IntertwiningMap σ) : (Representation.IntertwiningMap.toLinearMapl ρ σ) self = self.toLinearMap
• 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.IntertwiningMap.isIntertwining_assoc 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Semiring 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) {f : ρ.IntertwiningMap σ} (g : G) (l : U →ₗ[A] V) : f.toLinearMap ∘ₗ ρ g ∘ₗ l = σ g ∘ₗ f.toLinearMap ∘ₗ l
• Representation.IntertwiningMap.centralAlgebraMul_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) {z : MonoidAlgebra A G} (hz : z ∈ Submonoid.center (MonoidAlgebra A G)) (v : V) : (Representation.IntertwiningMap.centralAlgebraMul ρ hz) v = (ρ.asAlgebraHom z) v
• LinearMap.toIntertwiningMap 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] (ρ : Representation A G V) (σ : Representation A G W) (f : V →ₗ[A] W) (hf : ∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)) (v : V) : (LinearMap.intertwiningMap_of_isIntertwiningMap ρ σ f hf) v = f v
• Representation.Equiv.toIntertwiningMap_mk' 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} (e : V ≃ₗ[A] W) (he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e) : ↑(Representation.Equiv.mk e he) = { toLinearMap := ↑e, isIntertwining' := he }
• Representation.IntertwiningMap.equivLinearMapAsModule 📋 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) : ρ.IntertwiningMap σ ≃ₗ[A] ρ.asModule →ₗ[MonoidAlgebra A G] σ.asModule
• Representation.IntertwiningMap.llcomp 📋 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) : σ.IntertwiningMap τ →ₗ[A] ρ.IntertwiningMap σ →ₗ[A] ρ.IntertwiningMap τ
• 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.IntertwiningMap.coprod_inl_inr 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring A] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module A V] [Module A W] {ρ : Representation A G V} {σ : Representation A G W} : (Representation.IntertwiningMap.inl A ρ σ).comp (Representation.IntertwiningMap.fst A ρ σ) + (Representation.IntertwiningMap.inr A ρ σ).comp (Representation.IntertwiningMap.snd A ρ σ) = Representation.IntertwiningMap.id (ρ.prod σ)
• 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.IntertwiningMap.centralAlgebraMulHom_apply 📋 Mathlib.RepresentationTheory.Intertwining
  {A : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring A] [Monoid G] [AddCommMonoid V] [Module A V] (ρ : Representation A G V) (z : ↥(Submonoid.center (MonoidAlgebra A G))) : (Representation.IntertwiningMap.centralAlgebraMulHom ρ) z = Representation.IntertwiningMap.centralAlgebraMul ρ ⋯
• Representation.IntertwiningMap.comp_def 📋 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 τ) (g : ρ.IntertwiningMap σ) : f.comp g = ((Representation.IntertwiningMap.llcomp ρ σ τ) f) g
• Representation.linearizeMap 📋 Mathlib.RepresentationTheory.Action
  {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X Y : Action (Type w) G} (f : X ⟶ Y) : (Representation.linearize k G X).IntertwiningMap (Representation.linearize k G Y)
• Representation.LinearizeMonoidal.ε 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (Representation.trivial k G k).IntertwiningMap (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type w) G)))
• Representation.LinearizeMonoidal.η 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G))).IntertwiningMap (Representation.trivial k G k)
• Representation.LinearizeMonoidal.η_ε 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (Representation.LinearizeMonoidal.η k G).comp (Representation.LinearizeMonoidal.ε k G) = Representation.IntertwiningMap.id (Representation.trivial k G k)
• Representation.linearizeMap_single 📋 Mathlib.RepresentationTheory.Action
  {k : Type u} {G : Type v} [Monoid G] [Semiring k] {X Y : Action (Type w) G} (f : X ⟶ Y) (x : X.V) (r : k) : (Representation.linearizeMap f) (MonoidAlgebra.single x r) = MonoidAlgebra.single ((CategoryTheory.ConcreteCategory.hom f.hom) x) r
• Representation.LinearizeMonoidal.ε_one 📋 Mathlib.RepresentationTheory.Action
  {k : Type u} {G : Type v} [Monoid G] [Semiring k] : (Representation.LinearizeMonoidal.ε k G) 1 = MonoidAlgebra.single PUnit.unit 1
• Representation.LinearizeMonoidal.η_single 📋 Mathlib.RepresentationTheory.Action
  {k : Type u} {G : Type v} [Monoid G] [Semiring k] (x : PUnit.{u + 1}) : (Representation.LinearizeMonoidal.η k G) (MonoidAlgebra.single x 1) = 1
• 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.ε_η 📋 Mathlib.RepresentationTheory.Action
  (k : Type u) (G : Type v) [Monoid G] [Semiring k] : (Representation.LinearizeMonoidal.ε k G).comp (Representation.LinearizeMonoidal.η k G) = Representation.IntertwiningMap.id (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Action (Type u) G)))
• 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.freeLift 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) {α : Type w'} (f : α → V) : (Representation.free k G α).IntertwiningMap σ
• Representation.leftRegularMapEquiv 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) : (Representation.leftRegular k G).IntertwiningMap σ ≃ₗ[k] V
• Representation.freeLiftLEquiv 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) (α : Type w') : (Representation.free k G α).IntertwiningMap σ ≃ₗ[k] α → V
• Representation.freeLift_single_single 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) {α : Type w'} (i : α) (g : G) (r : k) (f : α → V) : ((σ.freeLift f) fun₀ | i => MonoidAlgebra.single g r) = r • (σ g) (f i)
• Representation.leftRegularMapEquiv_apply 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) (f : (Representation.leftRegular k G).IntertwiningMap σ) : σ.leftRegularMapEquiv f = f (MonoidAlgebra.single 1 1)
• Representation.leftRegularMapEquiv_symm_single 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) (g : G) (v : V) : (σ.leftRegularMapEquiv.symm v) (MonoidAlgebra.single g 1) = (σ g) v
• Representation.leftRegularMapEquiv_symm_apply_toFun 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) (v : V) (x : MonoidAlgebra k G) : (σ.leftRegularMapEquiv.symm v) x = x.coeff.sum fun x r => r • (σ x) v
• Representation.freeLiftLEquiv_symm_apply 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) (α : Type w') (f : α → V) : (σ.freeLiftLEquiv α).symm f = σ.freeLift f
• Representation.freeLiftLEquiv_apply 📋 Mathlib.RepresentationTheory.Equiv
  {G : Type v} [Monoid G] {V : Type v'} [AddCommMonoid V] {k : Type u} [CommSemiring k] [Module k V] (σ : Representation k G V) (α : Type w') (f : (Representation.free k G α).IntertwiningMap σ) (i : α) : (σ.freeLiftLEquiv α) f i = f fun₀ | i => MonoidAlgebra.single 1 1
• Rep.Hom.hom 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A.Hom B) : A.ρ.IntertwiningMap B.ρ
• Rep.Hom.hom' 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (self : A.Hom B) : A.ρ.IntertwiningMap B.ρ
• Rep.Hom.Simps.hom 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A B : Rep.{w, u, v} k G) (f : A.Hom B) : A.ρ.IntertwiningMap B.ρ
• Rep.hom_bijective 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : Function.Bijective Rep.Hom.hom
• Rep.hom_injective 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : Function.Injective Rep.Hom.hom
• Rep.hom_surjective 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : Function.Surjective Rep.Hom.hom
• Rep.ofHom 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (f : ρ.IntertwiningMap σ) : Rep.of ρ ⟶ Rep.of σ
• Rep.homEquiv 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : (A ⟶ B) ≃ A.ρ.IntertwiningMap B.ρ
• Rep.Hom.ext 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} {inst✝ : Semiring k} {inst✝¹ : Monoid G} {A B : Rep.{w, u, v} k G} {x y : A.Hom B} (hom' : x.hom' = y.hom') : x = y
• Rep.Hom.ext_iff 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} {inst✝ : Semiring k} {inst✝¹ : Monoid G} {A B : Rep.{w, u, v} k G} {x y : A.Hom B} : x = y ↔ x.hom' = y.hom'
• Rep.hom_id 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A : Rep.{w, u, v} k G) : Rep.Hom.hom (CategoryTheory.CategoryStruct.id A) = Representation.IntertwiningMap.id A.ρ
• Rep.instConcreteCategoryIntertwiningMapVρ 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] : CategoryTheory.ConcreteCategory (Rep.{w, u, v} k G) fun A B => A.ρ.IntertwiningMap B.ρ
• Rep.hom_ext 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} {f g : A ⟶ B} (hf : Rep.Hom.hom f = Rep.Hom.hom g) : f = g
• Rep.hom_ext_iff 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} {f g : A ⟶ B} : f = g ↔ Rep.Hom.hom f = Rep.Hom.hom g
• Rep.reflectsIsomorphisms_forget 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] : (CategoryTheory.forget (Rep.{w, u, v} k G)).ReflectsIsomorphisms
• Rep.forget_obj 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A : Rep.{w, u, v} k G) : (CategoryTheory.forget (Rep.{w, u, v} k G)).obj A = ↑A
• Rep.ofHom_neg 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (f : ρ.IntertwiningMap σ) : Rep.ofHom (-f) = -Rep.ofHom f
• Rep.hom_ofHom 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (f : ρ.IntertwiningMap σ) : Rep.Hom.hom (Rep.ofHom f) = f
• Rep.ofHom_comp 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} {Z : Type w} [AddCommGroup Z] [Module k Z] {τ : Representation k G Z} (f : ρ.IntertwiningMap σ) (g : σ.IntertwiningMap τ) : Rep.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (Rep.ofHom f) (Rep.ofHom g)
• Rep.ofHom_zero 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} : Rep.ofHom 0 = 0
• Rep.hom_comp 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] (A B C : Rep.{w, u, v} k G) (f : A ⟶ B) (g : B ⟶ C) : Rep.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Rep.Hom.hom g).comp (Rep.Hom.hom f)
• Rep.neg_hom 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) : Rep.Hom.hom (-f) = -Rep.Hom.hom f
• Rep.ofHom_sum 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {ι : Type u'} {M N : Type v'} [AddCommGroup M] [AddCommGroup N] [Module k M] [Module k N] {σ : Representation k G M} {ρ : Representation k G N} (f : ι → σ.IntertwiningMap ρ) (s : Finset ι) : Rep.ofHom (∑ i ∈ s, f i) = ∑ i ∈ s, Rep.ofHom (f i)
• Rep.mkIso_hom_hom 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (e : ρ.Equiv σ) : Rep.Hom.hom (Rep.mkIso e).hom = ↑e
• Rep.epi_iff_surjective 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Ring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) : CategoryTheory.Epi f ↔ Function.Surjective ⇑(Rep.Hom.hom f)
• Rep.mono_iff_injective 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Ring k] [Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) : CategoryTheory.Mono f ↔ Function.Injective ⇑(Rep.Hom.hom f)
• Rep.sum_hom 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} {ι : Type u'} (f : ι → (A ⟶ B)) (s : Finset ι) : Rep.Hom.hom (∑ i ∈ s, f i) = ∑ i ∈ s, Rep.Hom.hom (f i)
• Rep.trivialFunctor_map_hom 📋 Mathlib.RepresentationTheory.Rep.Basic
  (k : Type u) (G : Type v) [Ring k] [Monoid G] {X✝ Y✝ : ModuleCat k} (f : X✝ ⟶ Y✝) : Rep.Hom.hom ((Rep.trivialFunctor k G).map f) = { toLinearMap := ModuleCat.Hom.hom f, isIntertwining' := ⋯ }
• Rep.zero_hom 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {A B : Rep.{w, u, v} k G} : Rep.Hom.hom 0 = 0
• Rep.ofHom_zsmul 📋 Mathlib.RepresentationTheory.Rep.Basic
  {k : Type u} {G : Type v} [Semiring k] [Monoid G] {X Y : Type w} [AddCommGroup X] [AddCommGroup Y] [Module k X] [Module k Y] {ρ : Representation k G X} {σ : Representation k G Y} (f : ρ.IntertwiningMap σ) (n : ℤ) : Rep.ofHom (n • f) = n • Rep.ofHom f

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