intCast_cast_neg

Mathlib.Data.ZMod.Basic

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

English

For x ∈ ZMod n, the integer cast of −x equals − cast(x) mod n.

Русский

Для x ∈ ZMod n целочисленное представление −x равно − cast(x) mod n.

LaTeX

$$$\forall x \in \mathbb{Z}/n\mathbb{Z},\ (\operatorname{cast}(-x) : \mathbb{Z}) = -\operatorname{cast}(x) \bmod n$$$

Lean4

theorem intCast_cast_neg (x : ZMod n) : (cast (-x) : ℤ) = -cast x % n := by
  rw [← ZMod.coe_intCast, Int.cast_neg, ZMod.intCast_zmod_cast]

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

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

Разделы

Аффилиация

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