Theorem Fin.prod_Icc_castAdd

Modification history

2025-05-15 20:21
Mathlib/Algebra/BigOperators/Fin.lean
feat(BigOperators/Fin): lemmas about summation over intervals (#24358) …
Added Fin.prod_Icc_castAddView on Github →