Theorem Subgroup.mem_sup_of_normal_right

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_rightView on Github →