English
Let R be a ring with partial order and IsOrderedRing, and NoZeroDivisors holds. Then the interval [0,1] inside R forms a CancelMonoidWithZero under multiplication.
Русский
Пусть R — кольцо с частичным порядком и IsOrderedRing, и выполняется условие NoZeroDivisors. Тогда интервал [0,1] внутри R образует CancelMonoidWithZero по умножению.
LaTeX
$$$\text{If } R \text{ is a ring with } [\text{PartialOrder}] \text{ and } \text{NoZeroDivisors } R, \; (Icc(0,1)) \text{ is a CancelMonoidWithZero.}$$$
Lean4
instance instCancelMonoidWithZero {R : Type*} [Ring R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] :
CancelMonoidWithZero (Icc (0 : R) 1) :=
fast_instance%@Function.Injective.cancelMonoidWithZero R _ NoZeroDivisors.toCancelMonoidWithZero _ _ _ _
(fun v => v.val) Subtype.coe_injective coe_zero coe_one coe_mul coe_pow
