Commit 2024-06-01 08:19 5b761f86

View on Github →

chore: Split Algebra.BigOperators.Basic (#13277) ... into two files:

Algebra.BigOperators.Group.Finset for lemmas about group-like objects.
Algebra.BigOperators.GroupWithZero.Finset for lemmas about group-with-zero-like objects. Credit Johannes for https://github.com/leanprover-community/mathlib/commit/edfbf3cf.

Estimated changes

Modified Archive/Wiedijk100Theorems/InverseTriangleSum.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Defs.lean

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Renamed Mathlib/Algebra/BigOperators/Basic.lean to Mathlib/Algebra/BigOperators/Group/Finset.lean

deleted theorem Finset.prod_boole

deleted theorem Finset.prod_eq_zero

deleted theorem Finset.prod_eq_zero_iff

deleted theorem Finset.prod_ne_zero_iff

deleted theorem Finset.support_prod

deleted theorem Finset.support_prod_subset

deleted theorem Fintype.prod_boole

deleted theorem Units.mk0_prod

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

added theorem Finset.prod_boole

added theorem Finset.prod_eq_zero

added theorem Finset.prod_eq_zero_iff

added theorem Finset.prod_ne_zero_iff

added theorem Finset.support_prod

added theorem Finset.support_prod_subset

added theorem Fintype.prod_boole

added theorem Units.mk0_prod

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.lean

Modified Mathlib/Algebra/BigOperators/RingEquiv.lean

Modified Mathlib/Algebra/BigOperators/WithTop.lean

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

Modified Mathlib/Algebra/Order/Rearrangement.lean

Modified Mathlib/Algebra/Regular/Pow.lean

Modified Mathlib/Algebra/Star/BigOperators.lean

Modified Mathlib/Algebra/Tropical/BigOperators.lean

Modified Mathlib/Algebra/Vertex/HVertexOperator.lean

Modified Mathlib/CategoryTheory/Preadditive/Basic.lean

Modified Mathlib/CategoryTheory/Preadditive/Mat.lean

Modified Mathlib/Combinatorics/Additive/Dissociation.lean

Modified Mathlib/Combinatorics/HalesJewett.lean

Modified Mathlib/Combinatorics/SetFamily/Shatter.lean

Modified Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

Modified Mathlib/Data/Complex/BigOperators.lean

Modified Mathlib/Data/DFinsupp/Basic.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Finset/NoncommProd.lean

Modified Mathlib/Data/Finset/Slice.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/BigOperators.lean

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

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

Modified Mathlib/Data/Nat/GCD/BigOperators.lean

Modified Mathlib/Data/Rat/BigOperators.lean

Modified Mathlib/Data/Set/Pointwise/BigOperators.lean

Modified Mathlib/Data/Sym/Card.lean

Modified Mathlib/Deprecated/Submonoid.lean

Modified Mathlib/Dynamics/BirkhoffSum/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/BigOperators.lean

Modified Mathlib/GroupTheory/Index.lean

Modified Mathlib/LinearAlgebra/Lagrange.lean

Modified Mathlib/Order/Filter/AtTopBot.lean

Modified Mathlib/Order/Partition/Finpartition.lean

Modified Mathlib/RingTheory/Multiplicity.lean

Modified Mathlib/RingTheory/Prime.lean

Modified Mathlib/Tactic/NormNum/BigOperators.lean

Modified scripts/style-exceptions.txt

Modified test/apply_congr.lean

Modified test/linarith.lean