mathlib

e0f7d0e8 - feat(group_theory/complement): is_complement_iff_card_mul_and_disjoint (#9476)

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`).