Theorem hasProd_of_isLUB
Modification history
2025-07-19 23:06
Mathlib/Topology/Algebra/InfiniteSum/Order.lean
feat: remove unnecessary typeclass argument to Finset.prod lemmas for CanonicallyOrderedMul (#27294)
Modified hasProd_of_isLUBView on Github →2025-04-09 10:22
Mathlib/Topology/Algebra/InfiniteSum/Order.lean
chore: use mixin ordered algebraic typeclasses (part 2) (#20595)
Modified hasProd_of_isLUBView on Github →