Commit 2026-03-15 15:56 7a0d2c91

View on Github →

chore(WellFounded): drop unneeded Set.Nonempty assumptions (#35933) ... in theorems that also assume that a specific element belongs to the set.

Estimated changes

Modified Archive/Imo/Imo1988Q6.lean

Modified Counterexamples/AharoniKorman.lean

Modified Mathlib/Combinatorics/Quiver/Arborescence.lean

Modified Mathlib/Data/DFinsupp/WellFounded.lean

Modified Mathlib/FieldTheory/Minpoly/Basic.lean

Modified Mathlib/FieldTheory/SeparableClosure.lean

Modified Mathlib/FieldTheory/SeparablyGenerated.lean

Modified Mathlib/Order/Atoms.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Defs.lean

Modified Mathlib/Order/Cover.lean

Modified Mathlib/Order/InitialSeg.lean

Modified Mathlib/Order/OrderIsoNat.lean

Modified Mathlib/Order/PiLex.lean

Modified Mathlib/Order/SuccPred/Basic.lean

Modified Mathlib/Order/WellFounded.lean

modified theorem Function.argminOn_le

modified theorem Function.not_lt_argminOn

modified theorem WellFounded.not_lt_min

added theorem WellFounded.prop_min

Modified Mathlib/Order/WellFoundedSet.lean

Modified Mathlib/RingTheory/MvPowerSeries/LexOrder.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/ZFC/Class.lean

Modified Mathlib/Topology/EMetricSpace/Paracompact.lean