intCast_eq_zero_iff_even

Mathlib.Data.ZMod.Basic

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

English

An integer n maps to 0 in ZMod 2 precisely when n is even.

Русский

Целое число n отображается как 0 в ZMod 2 тогда и только тогда, когда n четное.

LaTeX

$$$ (n : ZMod 2) = 0 \iff \text{Even } n $$$

Lean4

theorem intCast_eq_zero_iff_even {n : ℤ} : (n : ZMod 2) = 0 ↔ Even n :=
  (CharP.intCast_eq_zero_iff (ZMod 2) 2 n).trans even_iff_two_dvd.symm

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

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

Разделы

Аффилиация

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