Mathlib v3 is deprecated. Go to Mathlib v4

Theorem associates.factors_self

Modification history

2022-02-23 10:50
src/ring_theory/unique_factorization_domain.lean
feat(ring_theory/unique_factorization_domain): add count_self (#12074)
Added associates.factors_selfView on Github →