Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-23 10:50 6179707b

View on Github →

feat(ring_theory/unique_factorization_domain): add count_self (#12074)

Estimated changes

Modified src/data/multiset/basic.lean

modified theorem multiset.count_singleton_self

Modified src/ring_theory/unique_factorization_domain.lean

added theorem associates.count_self

added theorem associates.factors_self