nat_mul_inj — Mathlib

English

For a ring R with NoZeroDivisors and CharZero, and any n ∈ ℕ, if (n : R)·a = (n : R)·b then n = 0 or a = b.

Русский

Для кольца R без нулевых делителей и характеристики нуля, для любого n ∈ ℕ, если $(n:R)\\cdot a=(n:R)\\cdot b$, то либо $n=0$, либо $a=b$.

LaTeX

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

Lean4

theorem nat_mul_inj {n : ℕ} {a b : R} (h : (n : R) * a = (n : R) * b) : n = 0 ∨ a = b :=
  by
  rw [← sub_eq_zero, ← mul_sub, mul_eq_zero, sub_eq_zero] at h
  exact mod_cast h

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