Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-10 23:30 8e92af1d

View on Github →

feat(algebra/associated): add lemmas to split #9345 (#10941) This PR contains lemmas from PR [#9345](https://github.com/leanprover-community/mathlib/pull/9345), which was starting to get quite lengthy.

Estimated changes

Modified src/algebra/associated.lean

added theorem associates.bot_eq_one

added theorem associates.le_one_iff

added theorem associates.mk_injective

added theorem dvd_not_unit.is_unit_of_irreducible_right

added theorem dvd_not_unit.ne

added theorem dvd_not_unit.not_associated

added theorem dvd_not_unit.not_unit

added theorem dvd_not_unit_of_dvd_not_unit_associated

added theorem is_unit_of_associated_mul

added theorem not_irreducible_of_not_unit_dvd_not_unit

added theorem not_is_unit_of_not_is_unit_dvd

added theorem pow_injective_of_not_unit

Modified src/algebra/divisibility.lean

added theorem ne_zero_of_dvd_ne_zero