Commit 2022-08-16 01:42 13482743
View on Github →chore(ring_theory/*): make ACC/DCC on rings be defeq to module versions (#15989)
This makes is_noetherian_ring R defeq to is_noetherian R R, and similar for is_artinian_ring. This was discussed on https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.40.5Breducible.5D.20defs.20of.20classes.20on.20the.20leadup.20to.20Lean4.2E.