Theorem tprod_one_sub_ordered

Modification history

2026-05-24 07:15
Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
perf: shortcut instances for `Semiring` (#39719) …
Modified tprod_one_sub_orderedView on Github →
2025-12-26 17:40
Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered (#30436) …
Added tprod_one_sub_orderedView on Github →