Commit 2024-11-04 10:03 5f98fda3

View on Github →

refactor(Multiset): drop Multiset.Disjoint (#18535) Use _root_.Disjoint instead.

Estimated changes

modified theorem MvPolynomial.le_degrees_add
modified theorem Multiset.sup_powerset_len
modified theorem Finset.disjoint_val
deleted theorem Multiset.Disjoint.symm
deleted def Multiset.Disjoint
modified theorem Multiset.coe_disjoint
deleted theorem Multiset.disjoint_comm
modified theorem Multiset.disjoint_left
modified theorem Multiset.zero_disjoint
modified theorem Multiset.Ico_disjoint_Ico