Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-08 00:26 b8971152

View on Github →

chore(algebra/associated): generalisation linter (#13108)

Estimated changes

Modified src/algebra/associated.lean

modified theorem associates.bot_eq_one

modified theorem associates.mk_injective

modified theorem associates.mk_one

modified theorem dvd_not_unit.is_unit_of_irreducible_right

modified theorem dvd_not_unit.not_unit

modified theorem dvd_not_unit_of_dvd_not_unit_associated

modified theorem not_irreducible_of_not_unit_dvd_not_unit