Theorem Subgroup.normalClosure_empty

Modification history

2026-02-18 13:53
Mathlib/Algebra/Group/Subgroup/Basic.lean
feat: the normal closure of an empty set is the trivial subgroup (#35029) …
Added Subgroup.normalClosure_emptyView on Github →