Commit 2024-08-23 14:42 a6864a3e

View on Github →

feat(RingTheory/Artinian): make IsArtinian an abbreviation for WellFoundedLT (#15797) We also tweak the IsNoetherian API analogously. This all improves code legibility quite a bit, and allows instance inference to be useful.

Estimated changes

Modified Mathlib/Algebra/DirectSum/LinearMap.lean

modified theorem LinearMap.trace_eq_zero_of_mapsTo_ne

Modified Mathlib/Algebra/Lie/Engel.lean

Modified Mathlib/Algebra/Lie/Nilpotent.lean

Modified Mathlib/Algebra/Lie/Solvable.lean

Modified Mathlib/Algebra/Lie/Subalgebra.lean

deleted theorem LieSubalgebra.wellFounded_of_noetherian

Modified Mathlib/Algebra/Lie/Submodule.lean

added theorem LieSubmodule.wellFoundedLT_of_isArtinian

deleted theorem LieSubmodule.wellFounded_of_isArtinian

deleted theorem LieSubmodule.wellFounded_of_noetherian

Modified Mathlib/Algebra/Lie/Weights/Basic.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Noetherian.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

Modified Mathlib/Order/ModularLattice.lean

Modified Mathlib/Order/RelIso/Basic.lean

Modified Mathlib/RingTheory/Artinian.lean

modified theorem IsArtinian.finite_of_linearIndependent

deleted theorem IsArtinian.wellFounded_submodule_lt

added theorem isArtinian_iff

deleted theorem isArtinian_iff_wellFounded

Modified Mathlib/RingTheory/Bezout.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/Localization/Submodule.lean

Modified Mathlib/RingTheory/Noetherian.lean

added theorem isNoetherian_iff'

added theorem isNoetherian_iff

deleted theorem isNoetherian_iff_wellFounded

deleted theorem wellFounded_submodule_gt

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean