cast_id

Mathlib.Data.ZMod.Basic

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

English

The canonical cast from ZMod n to itself is the identity map.

Русский

Канонический привод ZMod n в ZMod n является тождественным отображением.

LaTeX

$$$\\\\forall n : \\\\mathbb{N}, \\\\forall i : ZMod n, (ZMod.cast \\\\; i \\\\; : ZMod n) = i$$$

Lean4

theorem cast_id : ∀ (n) (i : ZMod n), (ZMod.cast i : ZMod n) = i
  | 0, _ => Int.cast_id
  | _ + 1, i => natCast_zmod_val i

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

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

Разделы

Аффилиация

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