Commit 2025-05-01 06:42 14fb067c

View on Github →

chore(BigOperators/Fin): sections, type variables (#24197) General cleanup:

  • use M instead of Greek letters for the codomain of lemmas about products and sums;
  • move [CommMonoid M] to variable;
  • rename Fin.prod_univ_get to Fin.prod_univ_getElem, similarly for the additive version;
  • rename Fin.prod_univ_get' to Fin.prod_univ_fun_getElem, similarly for the additive version;
  • add a missing to_additive for Fin.prod_const;

Estimated changes

modified theorem Fin.prod_Ioi_succ
modified theorem Fin.prod_Ioi_zero
modified theorem Fin.prod_congr'
modified theorem Fin.prod_cons
modified theorem Fin.prod_const
modified theorem Fin.prod_ofFn
modified theorem Fin.prod_snoc
modified theorem Fin.prod_trunc
modified theorem Fin.prod_univ_add
modified theorem Fin.prod_univ_castSucc
modified theorem Fin.prod_univ_def
modified theorem Fin.prod_univ_eight
modified theorem Fin.prod_univ_five
modified theorem Fin.prod_univ_four
deleted theorem Fin.prod_univ_get'
deleted theorem Fin.prod_univ_get
added theorem Fin.prod_univ_getElem
modified theorem Fin.prod_univ_one
modified theorem Fin.prod_univ_seven
modified theorem Fin.prod_univ_six
modified theorem Fin.prod_univ_succ
modified theorem Fin.prod_univ_succAbove
modified theorem Fin.prod_univ_three
modified theorem Fin.prod_univ_two'
modified theorem Fin.prod_univ_two
modified theorem Fin.prod_univ_zero
deleted theorem Fin.sum_const
modified theorem Finset.prod_range