zmod_injective — Mathlib

English

The map x ↦ zmod n x is injective; i.e., zmod n x = zmod n y implies x = y.

Русский

Отображение x ↦ zmod n x инъективно; если zmod n x = zmod n y, то x = y.

LaTeX

$$$ zmod(n)\, x = zmod(n)\, y \Rightarrow x=y $$$

Lean4

theorem zmod_injective : Injective (zmod n) :=
  by
  simp_rw [Injective, ZMod.intCast_surjective.forall]
  rintro x y h
  have hn : (n : ℝ) ≠ 0 := NeZero.ne _
  simpa [pi_ne_zero, exp_inj, hn, CharP.intCast_eq_intCast (ZMod n) n] using
    (zmod_intCast ..).symm.trans <| (DFunLike.congr_fun h ((1 : ℤ) : ZMod n)).trans <| zmod_intCast ..

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