Theorem isNoetherian_of_fg_of_noetherian'

Modification history

2023-08-16 16:40

Mathlib/RingTheory/Noetherian.lean

chore: restate `isNoetherian_of_fg_of_noetherian'` using `Module.Finite` (and rename). (#6609)

Deleted isNoetherian_of_fg_of_noetherian'View on Github →

2023-03-20 19:32

Mathlib/RingTheory/Noetherian.lean

feat: port RingTheory.Noetherian (#2976)

Added isNoetherian_of_fg_of_noetherian'View on Github →