Commit 2023-11-03 10:44 0030ea77

View on Github →

feat: Shorthands for well-foundedness of < and > (#7865) We already have WellFoundedLT/WellFoundedGT as wrappers around IsWellFounded, but we didn't have the corresponding wrapper lemmas.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

Modified Mathlib/Data/Multiset/Basic.lean

deleted theorem Multiset.wellFounded_lt

Modified Mathlib/Data/Nat/PartENat.lean

Modified Mathlib/Data/Polynomial/Degree/Definitions.lean

Modified Mathlib/Data/Polynomial/Degree/TrailingDegree.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

modified theorem sInf_eq_argmin_on

Modified Mathlib/Order/RelClasses.lean

added theorem wellFounded_gt

added theorem wellFounded_lt

Modified Mathlib/Order/WithBot.lean

deleted theorem WithBot.wellFounded_gt

deleted theorem WithBot.wellFounded_lt

deleted theorem WithTop.wellFounded_gt

deleted theorem WithTop.wellFounded_lt

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/Int/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean