zero

Mathlib.Algebra.Group.EvenFunction

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

English

The zero function is odd: for all x, f(-x) = -f(x).

Русский

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

LaTeX

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

Lean4

/-- The zero function is odd. -/
theorem zero [NegZeroClass β] : Function.Odd (fun (_ : α) ↦ (0 : β)) := fun _ ↦ neg_zero.symm

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

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

Разделы

Аффилиация

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