Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-03 20:00 5541b256

View on Github →

refactor(group_theory/complement): Introduce abbreviation for subgroups (#10009) Introduces abbreviation for is_complement (H : set G) (K : set G).

Estimated changes

Modified src/group_theory/complement.lean

added theorem subgroup.is_complement'.card_mul

added theorem subgroup.is_complement'.disjoint

added theorem subgroup.is_complement'.symm

added def subgroup.is_complement'

added theorem subgroup.is_complement'_comm

added theorem subgroup.is_complement'_def

added theorem subgroup.is_complement'_iff_card_mul_and_disjoint

added theorem subgroup.is_complement'_of_card_mul_and_disjoint

added theorem subgroup.is_complement'_of_coprime

deleted theorem subgroup.is_complement.card_mul

deleted theorem subgroup.is_complement.disjoint

deleted theorem subgroup.is_complement.symm

deleted theorem subgroup.is_complement_comm

deleted theorem subgroup.is_complement_iff_card_mul_and_disjoint

deleted theorem subgroup.is_complement_of_card_mul_and_disjoint

deleted theorem subgroup.is_complement_of_coprime

Modified src/group_theory/schur_zassenhaus.lean

added theorem subgroup.exists_left_complement'_of_coprime

deleted theorem subgroup.exists_left_complement_of_coprime

added theorem subgroup.exists_right_complement'_of_coprime

deleted theorem subgroup.exists_right_complement_of_coprime

added theorem subgroup.is_complement'_stabilizer_of_coprime

deleted theorem subgroup.is_complement_stabilizer_of_coprime