Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-04 05:40 70245f43

View on Github →

feat(algebra/big_operators): prod_comp (#2594) This is a lemma that @jcommelin looks like he could have used in Chevalley Warning, and is probably useful elsewhere.

Estimated changes