Commit 2025-01-06 23:47 213762fb

View on Github →

chore: don't import algebra in Data.Multiset.Basic (#19775)

Estimated changes

added theorem Multiset.addHom_ext
added def Multiset.cardHom
added theorem Multiset.card_nsmul
added theorem Multiset.countP_nsmul
added theorem Multiset.count_nsmul
added theorem Multiset.filter_nsmul
added theorem Multiset.map_nsmul
added theorem Multiset.mem_nsmul
added theorem Multiset.nsmul_cons
deleted theorem Multiset.addHom_ext
deleted def Multiset.cardHom
modified theorem Multiset.card_add
deleted theorem Multiset.card_nsmul
deleted theorem Multiset.countP_nsmul
deleted theorem Multiset.count_nsmul
modified theorem Multiset.eq_union_left
modified theorem Multiset.erase_add_left_neg
deleted theorem Multiset.filter_nsmul
modified theorem Multiset.le_add_left
modified theorem Multiset.le_add_right
modified theorem Multiset.le_union_left
deleted theorem Multiset.map_nsmul
deleted theorem Multiset.mem_nsmul
deleted theorem Multiset.mem_of_mem_nsmul
deleted theorem Multiset.nsmul_cons
deleted theorem Multiset.nsmul_replicate
deleted theorem Multiset.nsmul_singleton