Commit 2023-02-01 16:48 f0a4e27e

View on Github →

feat: port Algebra.BigOperators.Fin (#1848)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/BigOperators/Fin.lean

added def Fin.partialProd

added theorem Fin.partialProd_left_inv

added theorem Fin.partialProd_right_inv

added theorem Fin.partialProd_succ'

added theorem Fin.partialProd_succ

added theorem Fin.partialProd_zero

added theorem Fin.prod_congr'

added theorem Fin.prod_cons

added theorem Fin.prod_const

added theorem Fin.prod_ioi_succ

added theorem Fin.prod_ioi_zero

added theorem Fin.prod_ofFn

added theorem Fin.prod_trunc

added theorem Fin.prod_univ_add

added theorem Fin.prod_univ_castSucc

added theorem Fin.prod_univ_def

added theorem Fin.prod_univ_eight

added theorem Fin.prod_univ_five

added theorem Fin.prod_univ_four

added theorem Fin.prod_univ_one

added theorem Fin.prod_univ_seven

added theorem Fin.prod_univ_six

added theorem Fin.prod_univ_succ

added theorem Fin.prod_univ_succAbove

added theorem Fin.prod_univ_three

added theorem Fin.prod_univ_two

added theorem Fin.prod_univ_zero

added theorem Fin.sum_const

added theorem Fin.sum_pow_mul_eq_add_pow

added theorem Finset.prod_range

added theorem List.alternatingProd_eq_finset_prod

added theorem List.alternatingSum_eq_finset_sum

added theorem List.prod_ofFn

added theorem List.prod_take_ofFn

Modified Mathlib/Lean/Expr/Basic.lean

added def Lean.Expr.isConstantApplication

Modified Mathlib/Order/RelIso/Basic.lean

Modified Mathlib/Tactic/ToAdditive.lean

Modified test/toAdditive.lean

added def Test.myFin.foo

added def Test.myFin