Theorem one_le_finprod'

Modification history

2026-02-21 12:00

Mathlib/Algebra/BigOperators/Finprod.lean

chore: weaken `PartialOrder` to `Preorder` in `IsOrderedMonoid` hypothesis (#34295) …

Modified one_le_finprod'View on Github →

2025-04-04 17:16

Mathlib/Algebra/BigOperators/Finprod.lean

chore: use mixin ordered algebraic typeclasses (part 1) (#20594)

Modified one_le_finprod'View on Github →

2023-08-10 19:52

Mathlib/Algebra/BigOperators/Finprod.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified one_le_finprod'View on Github →

2023-01-23 14:15

Mathlib/Algebra/BigOperators/Finprod.lean

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

Added one_le_finprod'View on Github →