Commit 2025-05-15 10:23 5f07665f

feat(RepresentationTheory/*): subrepresentations, quotients by subrepresentations, and representations of quotient groups (#22651) Given a G-representation (V, ρ) and a G-invariant submodule W ≤ V, this PR defines the restriction of ρ to W as a representation, and the representation on V / W induced by ρ. When S is a normal subgroup of G on which ρ is trivial, we also define the G / S representation induced by ρ. We use this to define the G / S representation on V^S. We also add Representation.self_inv_apply, Representation.inv_self_apply, which supercede the following lemmas: Deletions:

• FDRep.inv_ρ_self_apply
• FDRep.ρ_inv_self_apply
• Rep.inv_ρ_self_apply
• Rep.ρ_inv_self_apply