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) …
Added finprod_le_finprod₀View on Github →