Theorem isNoetherian_of_isNoetherianRing_of_finite

Modification history

2023-12-13 18:20
Mathlib/RingTheory/Noetherian.lean
feat: make isNoetherian_of_isNoetherianRing_of_finite an instance (#8999) …
Deleted isNoetherian_of_isNoetherianRing_of_finiteView on Github →
2023-08-16 16:40
Mathlib/RingTheory/Noetherian.lean
chore: restate `isNoetherian_of_fg_of_noetherian'` using `Module.Finite` (and rename). (#6609)
Added isNoetherian_of_isNoetherianRing_of_finiteView on Github →