instIsAddTorsionFree — Mathlib

English

The natural numbers under addition have no nontrivial torsion: for every nonzero n, the map x ↦ n · x is injective, i.e. if n · x = n · y then x = y.

Русский

У натуральных чисел по сложению нет ненулевой торсии: для любого ненулевого n отображение x ↦ n·x инъективно, то есть если n·x = n·y, то x = y.

LaTeX

$$$\forall a,b,n \in \mathbb{N},\ (n \neq 0 \land n a = n b) \Rightarrow a=b$$$

Lean4

instance instIsAddTorsionFree : IsAddTorsionFree ℕ where
  nsmul_right_injective _n hn _x _y hxy := Nat.mul_left_cancel (Nat.pos_of_ne_zero hn) hxy

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