zero

Mathlib.Algebra.Group.EvenFunction

URI: https://scilib.ai/kg/mathlib#Function.Even.zero

English

The zero function is even: for all x, f(x)=0 satisfies f(-x)=f(x).

Русский

Нулевая функция чётна: для всех x выполняется f(-x)=f(x) при f(x)=0.

LaTeX

$$Even(\lambda x.0)$$

Lean4

/-- The zero function is even. -/
theorem zero [Zero β] : Function.Even (fun (_ : α) ↦ (0 : β)) :=
  Even.const 0

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

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

Разделы

Аффилиация

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