Commit 2025-06-12 10:35 15af5474

View on Github →

chore(Data/Set/Basic): deprecate lemmas that abuse the Set α := α → Prop defeq (#25669)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Associated.lean

Modified Mathlib/Algebra/Polynomial/EraseLead.lean

Modified Mathlib/CategoryTheory/Sites/Pretopology.lean

Modified Mathlib/Combinatorics/SimpleGraph/Diam.lean

modified theorem SimpleGraph.mem_center_iff

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/Data/Fintype/List.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/FieldTheory/AxGrothendieck.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean

Modified Mathlib/NumberTheory/SumPrimeReciprocals.lean

Modified Mathlib/RingTheory/KrullDimension/Basic.lean

Modified Mathlib/Topology/OmegaCompletePartialOrder.lean