natCast_val

Mathlib.Data.ZMod.Basic

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

English

For any i ∈ ZMod n, the R-value of i.val equals cast i.

Русский

Для любого i ∈ ZMod n, значение в R числа i.val равно приведения i.

LaTeX

$$$\\\\forall {n : \\\\mathbb{N}} (R : Type*) [Ring R] [NeZero n] (i : ZMod n), (i.\\\\val : R) = cast i$$

Lean4

@[simp]
theorem natCast_val [NeZero n] (i : ZMod n) : (i.val : R) = cast i :=
  congr_fun (natCast_comp_val R) i

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

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

Разделы

Аффилиация

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