English
Let α be a type equipped with a multiplication and a zero, and assume α is a subsingleton. Then multiplication by a nonzero element is cancellative on both sides: for all a ≠ 0 and all b,c in α, if a·b = a·c then b = c; and for all b ≠ 0 and all a,c in α, if b·a = c·a then b = c.
Русский
Пусть α — множество с умножением и нулём, обладающее единственным элементом. Тогда умножение на ненулевой элемент обладает отменой слева и справа: если a ≠ 0 и a·b = a·c, то b = c; если b ≠ 0 и b·a = c·a, то b = c.
LaTeX
$$$$\\bigl(\\forall a,b,c \in \\alpha,\\ a \\neq 0 \\rightarrow a b = a c \\rightarrow b=c\\bigr) \\,\\land\\,\n\\bigl(\\forall a,b,c \\in \\alpha,\\ b \\neq 0 \\rightarrow b a = c a \\rightarrow b=c\\bigr).$$$$
Lean4
instance to_isCancelMulZero [Mul α] [Zero α] [Subsingleton α] : IsCancelMulZero α
where
mul_right_cancel_of_ne_zero hb := (hb <| Subsingleton.eq_zero _).elim
mul_left_cancel_of_ne_zero hb := (hb <| Subsingleton.eq_zero _).elim
