Theorem Subgroup.normalClosure_eq_bot_iff

Modification history

2026-05-10 10:59
Mathlib/Algebra/Group/Subgroup/Basic.lean
chore(GroupTheory/SpecificGroups/Alternating): deprecate old proof of simplicity of A_5 (#38670) …
Added Subgroup.normalClosure_eq_bot_iffView on Github →