Commit 2025-04-26 23:10 99dfc6ca
View on Github →feat(Algebra/BigOperators): simprocify prod_univ_one/two/three/... (#23425)
Add a simproc prod_univ_many that rewrites ∏ (i : Fin n), f i as f 0 * f 1 * ... * f (n - 1), generalizing prod_univ_one, prod_univ_two, ..., prod_univ_eight.