val_cast_of_lt

Mathlib.Data.ZMod.Basic

URI: https://scilib.ai/kg/mathlib#ZMod.val_cast_of_lt

English

If a < n, then (a : ZMod n).val = a.

Русский

Если a < n, то (a : ZMod n).val = a.

LaTeX

$$$\text{If } a < n:\; (a : \mathbb{Z}/n\mathbb{Z}).\text{val} = a$$$

Lean4

theorem val_cast_of_lt {n : ℕ} {a : ℕ} (h : a < n) : (a : ZMod n).val = a := by rw [val_natCast, Nat.mod_eq_of_lt h]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru