Commit 2025-04-10 03:41 443f79b5

View on Github →

chore: split Algebra.BigOperators.Group.Finset.Basic (#23897) Split off

  • .Piecewise for the interaction of big operators with ite, dite and Finset.piecewise
  • .Indicator for the interaction of big operators with (mul)indicator
  • .Lemmas for four miscellaneous lemmas that were the only use of three imports in .Basic

Estimated changes

deleted theorem Finset.card_filter
deleted theorem Finset.dvd_prod_of_mem
deleted theorem Finset.isSquare_prod
deleted theorem Finset.mulIndicator_prod
deleted theorem Finset.mulSupport_prod
deleted theorem Finset.prod_apply_dite
deleted theorem Finset.prod_apply_ite
deleted theorem Finset.prod_dite
deleted theorem Finset.prod_dite_eq'
deleted theorem Finset.prod_dite_eq
deleted theorem Finset.prod_dite_of_false
deleted theorem Finset.prod_dite_of_true
modified theorem Finset.prod_eq_fold
deleted theorem Finset.prod_ite
deleted theorem Finset.prod_ite_eq'
deleted theorem Finset.prod_ite_eq
deleted theorem Finset.prod_ite_eq_of_mem
deleted theorem Finset.prod_ite_mem
deleted theorem Finset.prod_ite_of_false
deleted theorem Finset.prod_ite_of_true
deleted theorem Finset.prod_ite_one
deleted theorem Finset.prod_pi_mulSingle'
deleted theorem Finset.prod_pi_mulSingle
deleted theorem Finset.prod_piecewise
deleted theorem Finset.prod_pow_boole
deleted theorem Finset.prod_update_of_mem
deleted theorem Fintype.prod_dite_eq'
deleted theorem Fintype.prod_dite_eq
deleted theorem Fintype.prod_ite_eq'
deleted theorem Fintype.prod_ite_eq
deleted theorem Fintype.prod_ite_mem
modified theorem Fintype.prod_of_injective
deleted theorem Fintype.prod_pi_mulSingle
modified theorem IsCompl.prod_mul_prod
deleted theorem MonoidHom.coe_finset_prod
added theorem Finset.isSquare_prod
added theorem Finset.mulSupport_prod
added theorem Finset.card_filter
added theorem Finset.dvd_prod_of_mem
added theorem Finset.prod_apply_dite
added theorem Finset.prod_apply_ite
added theorem Finset.prod_dite
added theorem Finset.prod_dite_eq'
added theorem Finset.prod_dite_eq
added theorem Finset.prod_ite
added theorem Finset.prod_ite_eq'
added theorem Finset.prod_ite_eq
added theorem Finset.prod_ite_mem
added theorem Finset.prod_ite_one
added theorem Finset.prod_piecewise
added theorem Finset.prod_pow_boole
added theorem Fintype.prod_dite_eq'
added theorem Fintype.prod_dite_eq
added theorem Fintype.prod_ite_eq'
added theorem Fintype.prod_ite_eq
added theorem Fintype.prod_ite_mem