Commit 2026-04-05 08:48 664f0b3c

View on Github →

feat: 0 < a → 0 < a + b (#37641)

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

added theorem Left.one_lt_mul_of_left

added theorem Left.one_lt_mul_of_right

added theorem Right.one_lt_mul_of_left

added theorem Right.one_lt_mul_of_right

Modified Mathlib/SetTheory/Ordinal/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/Topology.lean

Modified Mathlib/SetTheory/Ordinal/Veblen.lean