Theorem AddSubgroup.mem_normalizer_iff_conj_image_eq

Modification history

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) …
Deleted AddSubgroup.mem_normalizer_iff_conj_image_eqView on Github →
2026-04-07 10:05
Mathlib/Algebra/Group/Subgroup/Basic.lean
feat(GroupTheory/Subgroup): basic API for set normalizers (#36760)
Added AddSubgroup.mem_normalizer_iff_conj_image_eqView on Github →