Theorem Subgroup.le_normalizer_iff_commutator_le_right

Modification history

2026-05-25 14:15
Mathlib/GroupTheory/Commutator/Basic.lean
feat(GroupTheory/Commutator/Basic): `⁅H₁, H₂⁆` is a normal subgroup of `H₁ ⊔ H₂` (#39227) …
Added Subgroup.le_normalizer_iff_commutator_le_rightView on Github →