Commit 2025-02-08 23:59 46ac7583

View on Github →

refactor(Order/OrderIsoNat): use WellFoundedGT in monotone chain condition (#20782) Instead of WellFounded (· > ·), we write WellFoundedGT α. We also add some docstrings, and one-sided versions of the theorem which take in WellFoundedGT α as a typeclass argument.

Estimated changes

Modified Mathlib/Algebra/Lie/Nilpotent.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

modified theorem Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex

Modified Mathlib/Order/OrderIsoNat.lean

added theorem WellFoundedGT.iSup_eq_monotonicSequenceLimit

added theorem WellFoundedGT.monotone_chain_condition'

added theorem WellFoundedGT.monotone_chain_condition

added theorem wellFoundedGT_iff_monotone_chain_condition'

added theorem wellFoundedGT_iff_monotone_chain_condition

Modified Mathlib/RingTheory/Artinian/Module.lean

Modified Mathlib/RingTheory/Noetherian/Defs.lean