val_injective — Mathlib

English

For any n, the function val: ZMod n → ℕ is injective; distinct residues have distinct representatives.

Русский

Для любого n функция val: ZMod n → ℕ инъективна; разные остатки дают разные представления.

LaTeX

$$$\forall n,\; \mathrm{Injective}\ (\mathrm{ZMod}.\mathrm{val})$$$

Lean4

theorem val_injective (n : ℕ) [NeZero n] : Function.Injective (val : ZMod n → ℕ) :=
  by
  cases n
  · cases NeZero.ne 0 rfl
  intro a b h
  dsimp [ZMod]
  ext
  exact h

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