English
Let R be a nontrivial linear ordered commutative semiring. Then the positive subset { x ∈ R | 0 < x } is a linear ordered cancellative monoid under multiplication.
Русский
Пусть R — ненулевой линейно упорядоченный коммутативный полусемирий. Тогда положительная часть образует линейно упорядоченную отменяемую моноид под умножением.
LaTeX
$$$\\\\text{IsOrderedCancelMonoid} \\\\{ x : R \\\\mid 0 < x \\\\}$ under multiplication.$$
Lean4
/-- If `R` is a nontrivial linear ordered commutative semiring, then `{x : R // 0 < x}` is a linear
ordered cancellative commutative monoid. -/
instance isOrderedCancelMonoid [CommSemiring R] [LinearOrder R] [IsStrictOrderedRing R] :
IsOrderedCancelMonoid { x : R // 0 < x } where le_of_mul_le_mul_left a _ _ := (mul_le_mul_iff_right₀ a.2).1
