Commit 2021-10-31 14:01 36de1ef6

View on Github →

chore(ring_theory/noetherian): generalize to semiring (#10032) This weakens some typeclasses on some results about is_noetherian (which already permits modules over semirings), and relaxes is_noetherian_ring to permit semirings. This does not actually try changing any of the proofs, it just relaxes assumptions that were stronger than what was actually used.

Estimated changes

Modified src/ring_theory/noetherian.lean

modified theorem is_noetherian_of_submodule_of_noetherian

modified theorem is_noetherian_of_tower

modified theorem is_noetherian_ring_iff

modified theorem is_noetherian_ring_iff_ideal_fg

modified theorem ring.is_noetherian_of_zero_eq_one

modified theorem well_founded_submodule_gt