mathlib3
1c07dc0e - feat(algebra/big_operators): `prod_ite_of_{true, false}`. (#7291)

Commit

4 years ago

feat(algebra/big_operators): `prod_ite_of_{true, false}`. (#7291) Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>

Author

ericrbg

Parents