even_iff_mod_of_even

Mathlib.Data.Fin.Parity

URI: https://scilib.ai/kg/mathlib#Fin.even_iff_mod_of_even

English

If n is even, then k is even iff k.val ≡ 0 mod 2.

Русский

Если n четно, то k четно тогда, когда k.val ≡ 0 по модулю 2.

LaTeX

$$$\forall \{n\,k\},\; (\mathrm{Even}(n)) \rightarrow (\mathrm{Even}(k) \iff k.\mathrm{val} \equiv 0 \pmod{2}).$$$

Lean4

theorem even_iff_mod_of_even (hn : Even n) : Even k ↔ k.val % 2 = 0 :=
  by
  rw [even_iff_of_even hn]
  exact Nat.even_iff

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

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

Разделы

Аффилиация

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