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]
tovariable
; - rename
Fin.prod_univ_get
toFin.prod_univ_getElem
, similarly for the additive version; - rename
Fin.prod_univ_get'
toFin.prod_univ_fun_getElem
, similarly for the additive version; - add a missing
to_additive
forFin.prod_const
;