Theorems · Theorem · group theory

Representation.FiniteCyclicGroup.coinvariantsKer_eq_range

∀ {k : Type u_1} {G : Type u_2} [inst : CommRing k] [inst_1 : Group G] {V : Type u_4} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G) [Finite G],
  (∀ (x : G), x ∈ Subgroup.zpowers g) → Representation.Coinvariants.ker ρ = (ρ g - LinearMap.id).range

Defined in

Mathlib.RepresentationTheory.Homological.FiniteCyclic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingGroupAddCommGroupModuleFinite