Commit 2026-02-25 23:34 78e57d26

View on Github →

chore(Finset): drop Membership instance (#35780) Use the one coming from SetLike instead.

Estimated changes

Modified Mathlib/Analysis/Convex/Radon.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean

Modified Mathlib/Combinatorics/SimpleGraph/Copy.lean

Modified Mathlib/Data/Finset/Defs.lean

Modified Mathlib/Data/Finset/NoncommProd.lean

Modified Mathlib/Data/Finset/Piecewise.lean

modified theorem Finset.piecewise_coe

Modified Mathlib/FieldTheory/Perfect.lean

Modified Mathlib/RingTheory/FiniteType.lean