instIsRightCancelMulZero — Mathlib

English

The ball inherits the right-cancellation property for multiplication: if b ≠ 0 and a·b = c·b with b in the ball, then a=c.

Русский

Единичная сфера наследует правую уникальность умножения: если b ≠ 0 и a·b = c·b, то a=c.

LaTeX

$$$\\forall a,b,c \\in \\text{ball}(0,1),\\; b\\neq 0 \\land ab=cb \\Rightarrow a=c$$$

Lean4

instance instIsRightCancelMulZero [NonUnitalSeminormedRing 𝕜] [IsRightCancelMulZero 𝕜] :
    IsRightCancelMulZero (ball (0 : 𝕜) 1) :=
  Subtype.val_injective.isRightCancelMulZero _ rfl fun _ _ ↦ rfl

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