Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.index_center_le_pow

Modification history

2022-11-15 10:09
src/group_theory/index.lean
feat(group_theory/group_action/quotient): If `G=<S>`, then `G / Z(G)` embeds into `S → {[g₁, g₂]}` (#17151) …
Added subgroup.index_center_le_powView on Github →