Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-10-24 11:00
31888cee
View on Github →
chore(Data):
SetLike Finset
(
#28241
)
Estimated changes
Modified
Counterexamples/AharoniKorman.lean
modified
theorem
Hollom.chainBetween_isChain
Modified
Mathlib/Algebra/BigOperators/Field.lean
modified
theorem
Finset.dens_biUnion
Modified
Mathlib/Algebra/BigOperators/Finprod.lean
Modified
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
modified
theorem
Finset.card_biUnion
Modified
Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
Modified
Mathlib/Algebra/GroupWithZero/Action/Pointwise/Finset.lean
Modified
Mathlib/Algebra/Module/FinitePresentation.lean
Modified
Mathlib/Algebra/MvPolynomial/Variables.lean
modified
theorem
MvPolynomial.aeval_ite_mem_eq_self
Modified
Mathlib/Algebra/Polynomial/Roots.lean
Modified
Mathlib/Algebra/Squarefree/Basic.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean
Modified
Mathlib/Analysis/Normed/Affine/Convex.lean
Modified
Mathlib/Combinatorics/Additive/RuzsaCovering.lean
Modified
Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
Modified
Mathlib/Combinatorics/SetFamily/LYM.lean
modified
theorem
Finset.lubell_yamamoto_meshalkin_inequality_sum_inv_choose
modified
theorem
IsAntichain.sperner
Modified
Mathlib/Combinatorics/SimpleGraph/Clique.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean
Modified
Mathlib/Data/DFinsupp/Defs.lean
Modified
Mathlib/Data/ENNReal/BigOperators.lean
Modified
Mathlib/Data/Finset/Attach.lean
modified
theorem
Finset.coe_attach
Modified
Mathlib/Data/Finset/Basic.lean
modified
def
Finset.equivToSet
Modified
Mathlib/Data/Finset/Defs.lean
modified
theorem
Finset.coe_ssubset
deleted
def
Finset.toSet
Modified
Mathlib/Data/Finset/Insert.lean
Modified
Mathlib/Data/Finset/Pi.lean
Modified
Mathlib/Data/Finset/Union.lean
Modified
Mathlib/Data/Set/Card.lean
Modified
Mathlib/Data/Set/Card/Arithmetic.lean
Modified
Mathlib/FieldTheory/Finite/GaloisField.lean
Modified
Mathlib/FieldTheory/Perfect.lean
Modified
Mathlib/GroupTheory/Finiteness.lean
Modified
Mathlib/GroupTheory/Perm/Centralizer.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Basic.lean
Modified
Mathlib/LinearAlgebra/Basis/Cardinality.lean
Modified
Mathlib/LinearAlgebra/Dimension/Constructions.lean
Modified
Mathlib/LinearAlgebra/Finsupp/Supported.lean
Modified
Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
Modified
Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
Modified
Mathlib/MeasureTheory/Integral/IntegrableOn.lean
Modified
Mathlib/MeasureTheory/Measure/Restrict.lean
Modified
Mathlib/ModelTheory/FinitelyGenerated.lean
Modified
Mathlib/ModelTheory/Semantics.lean
Modified
Mathlib/Order/CountableDenseLinearOrder.lean
Modified
Mathlib/Probability/Independence/InfinitePi.lean
Modified
Mathlib/Probability/Independence/Kernel.lean
Modified
Mathlib/Probability/Process/Filtration.lean
Modified
Mathlib/Probability/ProductMeasure.lean
Modified
Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean
Modified
Mathlib/RingTheory/Extension/Generators.lean
Modified
Mathlib/RingTheory/GradedAlgebra/FiniteType.lean
Modified
Mathlib/RingTheory/Ideal/Quotient/Index.lean
Modified
Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
Modified
Mathlib/RingTheory/Kaehler/Basic.lean
Modified
Mathlib/RingTheory/Noetherian/OfPrime.lean
Modified
Mathlib/RingTheory/Polynomial/ContentIdeal.lean
modified
def
Polynomial.contentIdeal
modified
theorem
Polynomial.contentIdeal_def
Modified
Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/SummationFilter.lean
Modified
Mathlib/Topology/ClopenBox.lean
Modified
Mathlib/Topology/Compactness/Bases.lean
Modified
Mathlib/Topology/Compactness/Compact.lean
Modified
Mathlib/Topology/DiscreteQuotient.lean
Modified
Mathlib/Topology/Instances/ENNReal/Lemmas.lean
Modified
Mathlib/Topology/Order/HullKernel.lean
Modified
Mathlib/Topology/Separation/Basic.lean