Theorem AddSubgroup.le_normalizer_closure_iff

Modification history

2026-05-27 15:09
Mathlib/Algebra/Group/Subgroup/Basic.lean
refactor(GroupTheory/*): additivize `AddAut` (#39884) …
Deleted AddSubgroup.le_normalizer_closure_iffView on Github →
2026-05-25 14:15
Mathlib/Algebra/Group/Subgroup/Basic.lean
feat(GroupTheory/Commutator/Basic): `⁅H₁, H₂⁆` is a normal subgroup of `H₁ ⊔ H₂` (#39227) …
Added AddSubgroup.le_normalizer_closure_iffView on Github →