Commit 2025-02-28 08:50 93207dce

View on Github →

chore: split Algebra/BigOperators/Group/Finset/Basic (#22261)

Estimated changes

Modified Mathlib.lean

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

deleted theorem Finset.card_sigma

deleted theorem Finset.prod_comm'

deleted theorem Finset.prod_comm

deleted theorem Finset.prod_finset_product'

deleted theorem Finset.prod_finset_product

deleted theorem Finset.prod_finset_product_right'

deleted theorem Finset.prod_finset_product_right

deleted theorem Finset.prod_preimage'

deleted theorem Finset.prod_preimage

deleted theorem Finset.prod_preimage_of_bij

deleted theorem Finset.prod_product'

deleted theorem Finset.prod_product

deleted theorem Finset.prod_product_right'

deleted theorem Finset.prod_product_right

deleted theorem Finset.prod_sigma'

deleted theorem Finset.prod_sigma

deleted theorem Finset.prod_univ_pi

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

added theorem Finset.prod_univ_pi

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

added theorem Finset.prod_preimage'

added theorem Finset.prod_preimage

added theorem Finset.prod_preimage_of_bij

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

added theorem Finset.card_sigma

added theorem Finset.prod_comm'

added theorem Finset.prod_comm

added theorem Finset.prod_finset_product'

added theorem Finset.prod_finset_product

added theorem Finset.prod_finset_product_right'

added theorem Finset.prod_finset_product_right

added theorem Finset.prod_product'

added theorem Finset.prod_product

added theorem Finset.prod_product_right'

added theorem Finset.prod_product_right

added theorem Finset.prod_sigma'

added theorem Finset.prod_sigma

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

Modified Mathlib/Algebra/BigOperators/Intervals.lean

Modified Mathlib/Algebra/BigOperators/NatAntidiagonal.lean

Modified Mathlib/Algebra/BigOperators/Option.lean

Modified Mathlib/Algebra/BigOperators/Pi.lean

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

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

Modified Mathlib/Algebra/BigOperators/Sym.lean

Modified Mathlib/Algebra/BigOperators/WithTop.lean

Modified Mathlib/Algebra/GradedMonoid.lean

Modified Mathlib/Algebra/Group/EvenFunction.lean

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

Modified Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean

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

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

Modified Mathlib/Algebra/Order/Rearrangement.lean

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

Modified Mathlib/Algebra/Tropical/BigOperators.lean

Modified Mathlib/CategoryTheory/Preadditive/Mat.lean

Modified Mathlib/Combinatorics/Additive/Dissociation.lean

Modified Mathlib/Combinatorics/HalesJewett.lean

Modified Mathlib/Combinatorics/Hindman.lean

Modified Mathlib/Combinatorics/SetFamily/Shatter.lean

Modified Mathlib/Data/Finset/NoncommProd.lean

Modified Mathlib/Data/Finset/Slice.lean

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Finsupp/BigOperators.lean

Modified Mathlib/Data/Fintype/BigOperators.lean

Modified Mathlib/Data/Holor.lean

Modified Mathlib/Data/Multiset/Fintype.lean

Modified Mathlib/Data/Nat/Factorial/DoubleFactorial.lean

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

Modified Mathlib/Data/Sym/Card.lean

Modified Mathlib/Dynamics/BirkhoffSum/Basic.lean

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

Modified Mathlib/GroupTheory/Perm/ClosureSwap.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/GroupTheory/Perm/Support.lean

Modified Mathlib/LinearAlgebra/Lagrange.lean

Modified Mathlib/ModelTheory/Definability.lean

Modified Mathlib/Order/Filter/AtTopBot/BigOperators.lean

Modified Mathlib/Order/LiminfLimsup.lean

Modified Mathlib/Order/Partition/Finpartition.lean

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

Modified Mathlib/RingTheory/Multiplicity.lean

Modified Mathlib/RingTheory/Prime.lean

Modified MathlibTest/linarith.lean