Theorems · Theorem · group theory

Representation.freeLiftLEquiv_symm_apply

∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {k : Type u} [inst_2 : CommSemiring k]
  [inst_3 : Module k V] (σ : Representation k G V) (α : Type w') (f : α → V), (σ.freeLiftLEquiv α).symm f = σ.freeLift f

Defined in

Mathlib.RepresentationTheory.Equiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidAddCommMonoidCommSemiringModule