instIsCancelMulZero — Mathlib

English

The unit disk with multiplication is cancelative for nonzero factors: if z ≠ 0 and z w1 = z w2, then w1 = w2.

Русский

Единичный диск с умножением обладает свойством отмены для ненулевых множителей: если z ≠ 0 и z w1 = z w2, то w1 = w2.

LaTeX

$$$\\\\forall z,w_1,w_2 \\\\in \\\\mathbb{D}, z \\neq 0 \\\\Rightarrow (z w_1 = z w_2 \\\\Rightarrow w_1 = w_2)$$$

Lean4

instance instIsCancelMulZero : IsCancelMulZero UnitDisc := by unfold UnitDisc; infer_instance

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