Theorem Subgroup.mem_sup_of_normal_left

Modification history

2025-11-14 17:31
Mathlib/Algebra/Group/Subgroup/Lattice.lean
feat: Subgroup.mem_sup for arbitrary groups when one of the subgroups is normal (#31458) …
Added Subgroup.mem_sup_of_normal_leftView on Github →