Commit 2022-12-31 05:31 f61ffad4
View on Github →chore(group_theory/coset): Additivise quotient_group.preimage_mk_equiv_subgroup_times_set (#18008)
The matches in the data fields were tripping to_additive up. Make one more argument to mk_mul_of_mem, fix the additive lemma name and remove a now useless argument to card_quotient_dvd_card.