cast_injective_of_le — Mathlib

English

If m ≤ n and m ≠ 0, then the natural cast from ZMod n to ZMod m is injective.

Русский

Если m ≤ n и m ≠ 0, то отображение приведения ZMod n → ZMod m инъективно.

LaTeX

$$$\forall m,n\ (m \le n)\ [NeZero m] \Rightarrow \operatorname{cast}: \mathbb{Z}/n\mathbb{Z} \to \mathbb{Z}/m\mathbb{Z} \text{ инъективно}$$$

Lean4

theorem cast_injective_of_le {m n : ℕ} [nzm : NeZero m] (h : m ≤ n) : Function.Injective (@cast (ZMod n) _ m) := by
  cases m with
  | zero => cases nzm; simp_all
  | succ m =>
    rintro ⟨x, hx⟩ ⟨y, hy⟩ f
    simp only [cast, val, natCast_eq_natCast_iff', Nat.mod_eq_of_lt (hx.trans_le h),
      Nat.mod_eq_of_lt (hy.trans_le h)] at f
    apply Fin.ext
    exact f

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