Commit 2025-12-11 22:59 c671bc42

View on Github →

chore: use Set.Nonempty everywhere (#32697)

Estimated changes

Modified Counterexamples/Phillips.lean

Modified Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean

added theorem Set.op_smul_inter_nonempty_iff

added theorem Set.smul_inter_nonempty_iff'

added theorem Set.smul_inter_nonempty_iff

Modified Mathlib/Algebra/Lie/Solvable.lean

Modified Mathlib/Algebra/Module/DedekindDomain.lean

Modified Mathlib/Algebra/Module/Torsion/Basic.lean

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

modified theorem AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree

Modified Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean

modified theorem Geometry.SimplicialComplex.convexHull_subset_space

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

Modified Mathlib/Order/Antichain.lean

Modified Mathlib/Order/Partition/Equipartition.lean

modified theorem Finpartition.top_isEquipartition

Modified Mathlib/Order/Preorder/Chain.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

Modified Mathlib/Topology/Connected/Clopen.lean

Modified Mathlib/Topology/NoetherianSpace.lean

added theorem TopologicalSpace.NoetherianSpace.exists_isOpen_nonempty_subset_irreducibleComponent