instIsCancelMulZero — Mathlib

English

Nimber satisfies cancellation laws: if a ≠ 0 and a*b = a*c, then b=c; similarly on the right.

Русский

Нимбер удовлетворяет законам отмены умножения: при a ≠ 0 и a*b = a*c следует b=c; аналогично слева.

LaTeX

$$$ a \neq 0 \implies a b = a c \Rightarrow b = c \\ and \\ a \neq 0 \implies b a = c a \Rightarrow b = c $$$

Lean4

instance : IsCancelMulZero Nimber
    where
  mul_left_cancel_of_ne_zero ha _ _
    h := by
    rw [← add_eq_zero, ← Nimber.mul_add, mul_eq_zero] at h
    exact add_eq_zero.1 (h.resolve_left ha)
  mul_right_cancel_of_ne_zero ha _ _
    h := by
    rw [← add_eq_zero, ← Nimber.add_mul, mul_eq_zero] at h
    exact add_eq_zero.1 (h.resolve_right ha)

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