Theorem finprod_apply_ne_one

Modification history

2025-01-13 10:02
Mathlib/Algebra/BigOperators/Finprod.lean
feat: `(∏ᶠ i, f i) a = ∏ᶠ i, f i a` (#20203) …
Added finprod_apply_ne_oneView on Github →