Commit 2021-08-19 12:44 802859f2

View on Github →

chore(algebra/big_operators): weaken assumption for multiset.exists_smul_of_dvd_count (#8758) This is slightly more convenient than doing a case split on a ∈ s in the caller.

Estimated changes

Modified src/algebra/big_operators/basic.lean

modified theorem multiset.exists_smul_of_dvd_count

Modified src/ring_theory/unique_factorization_domain.lean