cast_cast_zmod_of_le — Mathlib

English

If m ≤ n and a ∈ ZMod m, then casting a from ZMod m into ZMod n and back yields the original a: cast (cast a) = a.

Русский

Если m ≤ n и a ∈ ZMod m, то отображение a в ZMod n и обратно возвращает исходный элемент: cast (cast a) = a.

LaTeX

$$$ (cast (cast a : ZMod n) : ZMod m) = a $$$

Lean4

theorem cast_cast_zmod_of_le {m n : ℕ} [hm : NeZero m] (h : m ≤ n) (a : ZMod m) :
    (cast (cast a : ZMod n) : ZMod m) = a :=
  by
  have : NeZero n := ⟨((Nat.zero_lt_of_ne_zero hm.out).trans_le h).ne'⟩
  rw [cast_eq_val, val_cast_eq_val_of_lt (a.val_lt.trans_le h), natCast_zmod_val]

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