Commit 2025-03-03 07:17 95c78f35

View on Github →

feat: split long file Algebra.BigOperators.Group.Finset.Basic (#22476)

Estimated changes

Modified Archive/Imo/Imo2013Q1.lean

Modified Archive/Wiedijk100Theorems/InverseTriangleSum.lean

Modified Mathlib.lean

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

deleted theorem Finset.prod_powerset

deleted theorem Finset.prod_powersetCard

deleted theorem Finset.prod_powerset_cons

deleted theorem Finset.prod_powerset_insert

Created Mathlib/Algebra/BigOperators/Group/Finset/Powerset.lean

added theorem Finset.prod_powerset

added theorem Finset.prod_powersetCard

added theorem Finset.prod_powerset_cons

added theorem Finset.prod_powerset_insert

Modified Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean

Modified Mathlib/Algebra/BigOperators/Intervals.lean

Modified Mathlib/Algebra/BigOperators/Pi.lean

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

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

Modified Mathlib/Combinatorics/Additive/Dissociation.lean

Modified Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean

Modified Mathlib/Data/Fintype/CardEmbedding.lean

Modified Mathlib/Data/Holor.lean

Modified Mathlib/Data/Nat/Fib/Basic.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified MathlibTest/apply_congr.lean

Modified scripts/noshake.json