nat_mul_inj' — Mathlib

English

In a ring R with CharZero, multiplication by a nonzero natural number n is injective: if (n : R)·a = (n : R)·b and n ≠ 0, then a = b.

Русский

В кольце R с CharZero умножение на ненулевое натуральное число n инъективно: если $(n:R)\\cdot a=(n:R)\\cdot b$ и $n\\neq 0$, то $a=b$.

LaTeX

$$$(n : R) \\cdot a = (n : R) \\cdot b \\Rightarrow n \\neq 0 \\Rightarrow a = b$$$

Lean4

theorem nat_mul_inj' {n : ℕ} {a b : R} (h : (n : R) * a = (n : R) * b) (w : n ≠ 0) : a = b := by
  simpa [w] using nat_mul_inj h

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