instCancelCommMonoidWithZero — Mathlib

English

If R is a commutative ring with NoZeroDivisors, then the interval [0,1] in R forms a CancelCommMonoidWithZero under multiplication.

Русский

Если R — коммутативное кольцо без нулевых делителей, то интервал [0,1] в R образует CancelCommMonoidWithZero по умножению.

LaTeX

$$$\text{If } R \text{ is a commutative ring with no zero divisors, then } Icc(0,1) \text{ is a CancelCommMonoidWithZero under multiplication.}$$$

Lean4

instance instCancelCommMonoidWithZero {R : Type*} [CommRing R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] :
    CancelCommMonoidWithZero (Icc (0 : R) 1) :=
  fast_instance%@Function.Injective.cancelCommMonoidWithZero R _ NoZeroDivisors.toCancelCommMonoidWithZero _ _ _ _
      (fun v => v.val) Subtype.coe_injective coe_zero coe_one coe_mul coe_pow

Похожие утверждения