Theorem finprod_le_finprod

Modification history

2026-09-04 14:00
Mathlib/Algebra/BigOperators/Finprod.lean
chore(Algebra/Order/BigOperators): follow the `₀` naming convention (#39692) …
Modified finprod_le_finprodView on Github →
2026-01-29 07:34
Mathlib/Algebra/BigOperators/Finprod.lean
feat: add API lemmas for Multiset.prod_map and finprod (#34533) …
Added finprod_le_finprodView on Github →