instIsLeftCancelMulZero — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance instIsLeftCancelMulZero [NonUnitalSeminormedRing 𝕜] [IsLeftCancelMulZero 𝕜] :
    IsLeftCancelMulZero (ball (0 : 𝕜) 1) :=
  Subtype.val_injective.isLeftCancelMulZero _ rfl fun _ _ ↦ rfl

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