Theorem finprod_eq_prod

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_eq_prod View on Github →

2023-01-23 14:15

Mathlib/Algebra/BigOperators/Finprod.lean

feat: port Algebra.BigOperators.Finprod (#1766) …

Added finprod_eq_prod View on Github →