Theorem GroupExtension.Splitting.coe_monoidHom_mk

Modification history

2026-09-15 17:41

Mathlib/GroupTheory/GroupExtension/Defs.lean

chore(Algebra/MonoidHom): rename to `.ofClass` (#43755) …

Deleted GroupExtension.Splitting.coe_monoidHom_mk View on Github →

2025-01-17 06:22

Mathlib/GroupTheory/GroupExtension/Defs.lean

chore(GroupExtension/Defs): define `Section` and redefine `Splitting` (#20802) …

Added GroupExtension.Splitting.coe_monoidHom_mk View on Github →