Theorem finprod_option

Modification history

2026-03-03 17:54

Mathlib/Algebra/BigOperators/Finprod.lean

feat(Algebra/Group/FiniteSupport): add HasFinite(Mul)Support and API (#34658) …

Modified finprod_option View on Github →

2025-01-13 10:02

Mathlib/Algebra/BigOperators/Finprod.lean

feat: `(∏ᶠ i, f i) a = ∏ᶠ i, f i a` (#20203) …

Added finprod_option View on Github →