English
In a strictly ordered ring, multiplication by a nonzero element is injective: if a ≠ 0 and ab = ac, then b = c. Equivalently, for any a ≠ 0, the maps b ↦ ab and b ↦ ba are injective.
Русский
В строго упорядоченном кольце умножение на ненулевой элемент инъективно: если a ≠ 0 и ab = ac, то b = c. Аналогично для правого умножения.
LaTeX
$$$\\forall a,b,c\\in R,\\ a \\neq 0 \\ \\wedge\\ ab=ac \\Rightarrow b=c$$$
Lean4
instance (priority := 100) noZeroDivisors : NoZeroDivisors R where
eq_zero_or_eq_zero_of_mul_eq_zero {a b}
hab := by
contrapose! hab
obtain ha | ha := hab.1.lt_or_gt <;> obtain hb | hb := hab.2.lt_or_gt
exacts [(mul_pos_of_neg_of_neg ha hb).ne', (mul_neg_of_neg_of_pos ha hb).ne, (mul_neg_of_pos_of_neg ha hb).ne,
(mul_pos ha hb).ne']
-- Note that we can't use `NoZeroDivisors.to_isDomain` since we are merely in a semiring.
-- See note [lower instance priority]
