Commit 2024-10-07 17:59 4d57c2c0

View on Github →

feat: Noetherian/Artinian is closed under extensions (submodule form) (#17425)

  • Add isNoetherian/Artinian_iff_submodule_quotient.
  • Remove unnecessary assumptions from isArtinian_of_range_eq_ker, mimicking #12453.
  • Move up two instances isArtinian_of_quotient_of_artinian and isNoetherian_of_finite.
  • Golf isNoetherian/Artinian_pi.

Estimated changes