Mathlib Changelog
v4
Changelog
About
Github
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