Theorem Subgroup.Characteristic.comap_quotient_mk

Modification history

2026-02-16 08:27
Mathlib/GroupTheory/QuotientGroup/Basic.lean
feat(GroupTheory): each term in a upper(lower) central series is a characteristic subgroup (#34890) …
Added Subgroup.Characteristic.comap_quotient_mkView on Github →