Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-02 13:36 28443c8b

View on Github →

feat(ring_theory/noetherian): zero ring (and finite rings) are Noetherian (closes #341)

Estimated changes

Modified algebra/ring.lean

added theorem eq_zero_of_zero_eq_one

added theorem subsingleton_of_zero_eq_one

Modified data/polynomial.lean

added theorem polynomial.leading_coeff_eq_zero_iff_deg_eq_bot

Modified ring_theory/noetherian.lean

added theorem ring.is_noetherian_of_fintype

added theorem ring.is_noetherian_of_zero_eq_one