Commit 2026-05-25 14:15 66bbabfd

View on Github →

feat(GroupTheory/Commutator/Basic): ⁅H₁, H₂⁆ is a normal subgroup of H₁ ⊔ H₂ (#39227) Shows ⁅H₁, H₂⁆ ≤ H₁ ⊔ H₂ and (⁅H₁, H₂⁆.subgroupOf <| H₁ ⊔ H₂).Normal, and adds _ ≤ normalizer _ ↔ lemmas to help.

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

added theorem AddSubgroup.le_normalizer_closure_iff

added theorem AddSubgroup.mem_normalizer_iff_addConj_image_eq

deleted theorem AddSubgroup.mem_normalizer_iff_conj_image_eq

added theorem Subgroup.le_normalizer_closure_iff

added theorem Subgroup.le_normalizer_iff

added theorem Subgroup.le_set_normalizer_iff

Modified Mathlib/GroupTheory/Commutator/Basic.lean

added theorem Subgroup.commutator_le_sup

added theorem Subgroup.le_normalizer_iff_commutator_le_left

added theorem Subgroup.le_normalizer_iff_commutator_le_right

added theorem Subgroup.normalizer_commutator_ge_left

added theorem Subgroup.normalizer_commutator_ge_right

added theorem commutatorElement_mul_left_eq_conj_mul

added theorem commutatorElement_mul_right_eq_mul_conj