instCancelMonoid — Mathlib

English

The left and right cancellation laws hold for multiplication on Ioc(0,1) when appropriate ring properties are assumed.

Русский

При заданных свойствах кольца выполняются лево- и правоотмена для умножения на Ioc(0,1).

LaTeX

$$$\text{left cancel: } a\cdot b = a\cdot c \Rightarrow b=c$; $\text{right cancel: } b\cdot a = c\cdot a \Rightarrow b=c$$$

Lean4

instance instCancelMonoid {R : Type*} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [IsDomain R] :
    CancelMonoid (Ioc (0 : R) 1) :=
  {
    Set.Ioc.instMonoid with
    mul_left_cancel := fun a _ _ h => Subtype.ext <| mul_left_cancel₀ a.prop.1.ne' <| (congr_arg Subtype.val h :)
    mul_right_cancel := fun b _ _ h => Subtype.ext <| mul_right_cancel₀ b.prop.1.ne' <| (congr_arg Subtype.val h :) }

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