Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.quotient_centralizer_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_centralizer_embedding_apply View on Github →