Theorem finprod_of_not_hasFiniteMulSupport

Modification history

2026-03-03 17:54
Mathlib/Algebra/BigOperators/Finprod.lean
feat(Algebra/Group/FiniteSupport): add HasFinite(Mul)Support and API (#34658) …
Added finprod_of_not_hasFiniteMulSupportView on Github →