Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.quotient_center_embedding_apply

Modification history

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