val_add_of_lt — Mathlib

English

If a.val + b.val < n, then (a+b).val = a.val + b.val.

Русский

Если a.val + b.val < n, то (a+b).val = a.val + b.val.

LaTeX

$$$\forall a,b \in ZMod n\ (h:\ a.\mathrm{val} + b.\mathrm{val} < n)\Rightarrow (a+b).\mathrm{val} = a.\mathrm{val} + b.\mathrm{val}$$$

Lean4

theorem val_add_of_lt {n : ℕ} {a b : ZMod n} (h : a.val + b.val < n) : (a + b).val = a.val + b.val :=
  by
  have : NeZero n := by constructor; rintro rfl; simp at h
  rw [ZMod.val_add, Nat.mod_eq_of_lt h]

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