Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-14 10:14 743209ca

View on Github →

chore(algebra/big_operators/basic): spaces around binders (#8307)

Estimated changes

Modified src/algebra/big_operators/basic.lean

modified theorem finset.exists_ne_one_of_prod_ne_one

modified theorem finset.prod_congr

modified theorem finset.prod_eq_one

modified theorem finset.prod_eq_zero_iff

modified theorem finset.sum_const_nat