Commit 2021-10-01 06:05 e0f7d0e8

View on Github →

feat(group_theory/complement): is_complement_iff_card_mul_and_disjoint (#9476) Adds the converse to an existing lemma is_complement_of_disjoint (renamed is_complement_of_card_mul_and_disjoint).

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_iff_card_mul_and_disjoint

added theorem subgroup.is_complement_of_card_mul_and_disjoint

deleted theorem subgroup.is_complement_of_disjoint