Commit 2025-10-22 18:34 92204ffc

View on Github →

feat(GroupTheory/Index): criteria for subgroup to have index 2 (#30466) A few variations on the existing Subgroup.index_eq_two_iff.

Estimated changes

Modified Mathlib/GroupTheory/Index.lean

added theorem Subgroup.index_dvd_two_iff'

added theorem Subgroup.index_dvd_two_iff

added theorem Subgroup.index_eq_two_iff'

added theorem Subgroup.index_eq_two_iff_exists_notMem_and'

added theorem Subgroup.index_eq_two_iff_exists_notMem_and

added theorem Subgroup.relIindex_dvd_two_iff'

added theorem Subgroup.relIindex_eq_two_iff'

added theorem Subgroup.relIndex_dvd_two_iff

added theorem Subgroup.relIndex_eq_two_iff

added theorem Subgroup.relIndex_eq_two_iff_exists_notMem_and'

added theorem Subgroup.relIndex_eq_two_iff_exists_notMem_and