Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-23 14:30 1e0661ce

View on Github →

feat(ring_theory/noetherian): generalize to semiring (#9881) We generalize some of the results in ring_theory/noetherian to semiring.

Estimated changes

modified theorem module.finite.of_injective
modified theorem fg_of_injective
added theorem fg_of_ker_bot
modified theorem is_noetherian_of_injective
modified theorem submodule.fg_top