Commit 2026-02-27 13:07 a508a731

View on Github →

feat(RingTheory/Noetherian/Basic): semilinear generalizations (#35491) We show that if a semiring R is isomorphic to a Noetherian semiring S, then R is Noetherian. We also generalize much of the API of this file from linear maps to semilinear maps (some of the generalized lemmas are required for the above result).

Estimated changes

Modified Mathlib/Algebra/Lie/Engel.lean

Modified Mathlib/FieldTheory/Finiteness.lean

Modified Mathlib/RingTheory/FiniteLength.lean

Modified Mathlib/RingTheory/Finiteness/Quotient.lean

Modified Mathlib/RingTheory/Noetherian/Basic.lean

modified theorem LinearEquiv.isNoetherian_iff

modified theorem Module.Finite.of_injective

modified theorem fg_of_injective

modified theorem fg_of_ker_bot

modified theorem isNoetherian_iff_submodule_quotient

modified theorem isNoetherian_of_injective

modified theorem isNoetherian_of_ker_bot

modified theorem isNoetherian_of_linearEquiv

modified theorem isNoetherian_of_range_eq_ker

modified theorem isNoetherian_of_surjective