Commit 2024-03-25 07:55 d6a4b5d2

View on Github →

chore: Make Finset.preimage not depend on Finset.sum (#11601) and Data.Finset.LocallyFinite not depend on Finset.sum too

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

added theorem Finset.prod_preimage'

added theorem Finset.prod_preimage

added theorem Finset.prod_preimage_of_bij

Modified Mathlib/Algebra/BigOperators/Intervals.lean

added theorem Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag

Modified Mathlib/Algebra/BigOperators/Order.lean

Modified Mathlib/Analysis/Matrix.lean

Modified Mathlib/Combinatorics/SetFamily/Shatter.lean

Modified Mathlib/Data/Fin/Interval.lean

Modified Mathlib/Data/Finset/Antidiagonal.lean

Modified Mathlib/Data/Finset/LocallyFinite/Basic.lean

deleted theorem Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag

Modified Mathlib/Data/Finset/Preimage.lean

deleted theorem Finset.prod_preimage'

deleted theorem Finset.prod_preimage

deleted theorem Finset.prod_preimage_of_bij

Modified Mathlib/Data/Nat/Interval.lean

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/Order/Filter/AtTopBot.lean

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

Modified Mathlib/RingTheory/Multiplicity.lean

Modified Mathlib/Tactic/NormNum/BigOperators.lean

Modified test/linarith.lean