Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-12 04:01 e22789ef

View on Github →

feat(algebra/big_operators/finprod): add a few lemmas (#8261)

  • add finprod_eq_single and finsum_eq_single;
  • add finprod_induction and finsum_induction;
  • add single_le_finprod and single_le_finsum;
  • add one_le_finprod' and finsum_nonneg.

Estimated changes

added theorem finprod_eq_single
added theorem finprod_induction
added theorem one_le_finprod'
added theorem single_le_finprod