Commit 2025-04-02 01:39 1da0ec03

View on Github →

chore(*): use Finset.filter notation more (#23471) Also minor golf here and there.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

Modified Mathlib/Algebra/BigOperators/Intervals.lean

Modified Mathlib/Algebra/BigOperators/Ring/Nat.lean

Modified Mathlib/Algebra/DirectSum/Internal.lean

Modified Mathlib/Algebra/GCDMonoid/Finset.lean

Modified Mathlib/Algebra/Order/Antidiag/Pi.lean

Modified Mathlib/Algebra/Order/Antidiag/Prod.lean

Modified Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

Modified Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean

Modified Mathlib/Combinatorics/HalesJewett.lean

Modified Mathlib/Data/Finset/Density.lean

Modified Mathlib/Data/Finset/Interval.lean

modified theorem Finset.Icc_eq_filter_powerset

modified theorem Finset.Ico_eq_filter_ssubsets

modified theorem Finset.Ioc_eq_filter_powerset

modified theorem Finset.Ioo_eq_filter_ssubsets

Modified Mathlib/Data/Finset/NatAntidiagonal.lean

Modified Mathlib/Data/Finset/PImage.lean

Modified Mathlib/Data/Finset/Preimage.lean

Modified Mathlib/Data/List/ToFinsupp.lean

Modified Mathlib/Data/Multiset/Fintype.lean

Modified Mathlib/Data/Nat/Factorization/PrimePow.lean

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

Modified Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean

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

Modified Mathlib/NumberTheory/Bertrand.lean

Modified Mathlib/NumberTheory/Padics/PadicVal/Basic.lean

Modified Mathlib/NumberTheory/SmoothNumbers.lean

modified def Nat.primesBelow

modified theorem Nat.smoothNumbers_succ

Modified Mathlib/Order/CountableDenseLinearOrder.lean

Modified Mathlib/Probability/Distributions/Uniform.lean

Modified Mathlib/Topology/Algebra/Support.lean