mathlib
13482743 - chore(ring_theory/*): make ACC/DCC on rings be defeq to module versions (#15989)

Commit
3 years ago
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.
Author
Parents
Loading