val_cast_eq_val_of_lt — Mathlib

English

If a ∈ ZMod m satisfies a.val < n, then casting to ZMod n does not change the representative: (a.cast : ZMod n).val = a.val.

Русский

Пусть a ∈ ZMod m удовлетворяет a.val < n; тогда отображение в ZMod n не изменяет представление: (a.cast : ZMod n).val = a.val.

LaTeX

$$$ (a.cast : ZMod n).val = a.val $$$

Lean4

theorem val_cast_eq_val_of_lt {m n : ℕ} [nzm : NeZero m] {a : ZMod m} (h : a.val < n) : (a.cast : ZMod n).val = a.val :=
  by
  have nzn : NeZero n := by constructor; rintro rfl; simp at h
  cases m with
  | zero => cases nzm; simp_all
  | succ m =>
    cases n with
    | zero => cases nzn; simp_all
    | succ n => exact Fin.val_cast_of_lt h

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