Theorems · Theorem · group theory

Representation.leftRegularTensorTrivialIsoFree_apply_single_tmul_single

∀ {G : Type v} [inst : Monoid G] {k : Type u} [inst_1 : 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)

Defined in

Mathlib.RepresentationTheory.Equiv

Cited by

0 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidCommSemiring