intCast_abs_mod_two

Mathlib.Data.ZMod.Basic

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

English

The parity of an integer a is captured by equality (|a| mod 2) = a mod 2 in ZMod 2.

Русский

Паритет целого числа a задаётся равенством (|a| mod 2) = a mod 2 в ZMod 2.

LaTeX

$$$(|a|) \mod 2 = a \mod 2$ in ZMod 2$$

Lean4

@[simp]
theorem intCast_abs_mod_two (a : ℤ) : (↑|a| : ZMod 2) = a := by
  cases le_total a 0 <;> simp [abs_of_nonneg, abs_of_nonpos, *]

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

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

Разделы

Аффилиация

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