Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-17 13:47 9380977b

View on Github →

chore(algebra/big_operators/fin): moving lemmas (#13331) This PR moves lemmas about products and sums over fin n from data/fintype/card.lean to algebra/big_operators/fin.lean.

Estimated changes

added theorem fin.prod_const
added theorem fin.prod_of_fn
added theorem fin.prod_univ_def
added theorem fin.prod_univ_one
added theorem fin.prod_univ_succ
added theorem fin.prod_univ_two
added theorem fin.prod_univ_zero
added theorem fin.sum_const
added theorem finset.prod_range
added theorem list.prod_of_fn
added theorem list.prod_take_of_fn
deleted theorem fin.prod_const
deleted theorem fin.prod_of_fn
deleted theorem fin.prod_univ_cast_succ
deleted theorem fin.prod_univ_def
deleted theorem fin.prod_univ_one
deleted theorem fin.prod_univ_succ
deleted theorem fin.prod_univ_succ_above
deleted theorem fin.prod_univ_two
deleted theorem fin.prod_univ_zero
deleted theorem fin.sum_const
deleted theorem finset.prod_range
deleted theorem list.prod_of_fn
deleted theorem list.prod_take_of_fn