Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-03 16:58 1edb79ae

View on Github →

refactor(ring_theory/associated): rename associated_elements

Estimated changes

modified def irreducible
added theorem irreducible_or_factor
added theorem is_unit_iff_dvd_one
added theorem is_unit_iff_forall_dvd
added theorem is_unit_of_dvd_unit
added theorem of_irreducible_mul