Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-05 14:11 4e509a86

View on Github →

feat(ring_theory/noetherian): irreducible_induction_on (#563)

Estimated changes

Modified ring_theory/associated.lean

deleted theorem associates.zero_mul

added theorem dvd_and_not_dvd_iff

Modified ring_theory/ideals.lean

added theorem ideal.span_singleton_lt_span_singleton

Modified ring_theory/noetherian.lean

added theorem is_noetherian_ring.exists_irreducible_factor

added theorem is_noetherian_ring.irreducible_induction_on

added theorem is_noetherian_ring.well_founded_dvd_not_unit