mathlib

f61ffad4 - chore(group_theory/coset): Additivise `quotient_group.preimage_mk_equiv_subgroup_times_set` (#18008)

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