Mathlib v3 is deprecated. Go to Mathlib v4

Theorem associated_eq_eq

Modification history

2020-09-26 17:53
src/algebra/associated.lean
feat(data/nat/unique_factorization): a `unique_factorization_monoid` instance on N (#4194) …
Added associated_eq_eqView on Github →