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.
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.