instDecidablePredEven

Mathlib.Algebra.Group.Int.Even

URI: https://scilib.ai/kg/mathlib#Int.instDecidablePredEven

English

There exists a decision procedure for the predicate Even on ℤ.

Русский

Существует решение для четности целых чисел.

LaTeX

$$$\exists f:\\mathbb{Z} o \{0,1\},\ \forall n:\\mathbb{Z},\ f(n)=1 \Leftrightarrow \operatorname{Even}(n)$$$

Lean4

instance : DecidablePred (Even : ℤ → Prop) := fun _ ↦ decidable_of_iff _ even_iff.symm

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

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

Разделы

Аффилиация

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