Theorem Representation.Coinvariants.le_comap_ker

Modification history

2025-06-05 17:13
Mathlib/RepresentationTheory/Coinvariants.lean
feat(RepresentationTheory/Coinvariants): the `G ⧸ S`-representation on `A_S` for `A : Rep k G` (#22652) …
Added Representation.Coinvariants.le_comap_kerView on Github →