instCancelCommMonoid — Mathlib

English

Under a commutative domain, the multiplicative structure on Ioc(0,1) is cancelative and commutative.

Русский

При коммутативном области, умножение на Ioc(0,1) совместимо и допускает отмену.

LaTeX

$$$\text{CancelCommMonoid} (\text{Ioc}(0,1).\text{Elem})$$$

Lean4

instance instCancelCommMonoid {R : Type*} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [IsDomain R] :
    CancelCommMonoid (Ioc (0 : R) 1) :=
  { Set.Ioc.instCommMonoid, Set.Ioc.instCancelMonoid with }

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