Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-02 20:50 5f8fafcf

View on Github →

feat(ring_theory): add associated elements

Estimated changes

modified theorem mul_eq_zero
added theorem zero_eq_mul
added def associated
added theorem associates.dvd_out_iff
added theorem associates.is_unit_mk
added theorem associates.le_mul_left
added theorem associates.mk_mul_mk
added theorem associates.mk_zero_eq
added theorem associates.mul_mono
added theorem associates.mul_zero
added theorem associates.one_le
added theorem associates.out_dvd_iff
added theorem associates.out_mk
added theorem associates.out_mul
added theorem associates.out_one
added theorem associates.out_top
added theorem associates.prod_mk
added theorem associates.zero_mul
added theorem associates.zero_ne_one
added def associates
added def irreducible
added def is_unit
added theorem is_unit_mul_units
added theorem is_unit_nat
added theorem is_unit_one
added theorem not_irreducible_one
added theorem not_irreducible_zero
added theorem not_is_unit_zero