Odd

Mathlib.Algebra.Group.EvenFunction

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

Lean4

/-- A function `f` is _odd_ if it satisfies `f (-x) = -f x` for all `x`. -/
protected def Odd [Neg β] (f : α → β) : Prop :=
  ∀ a, f (-a) = -(f a)

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

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

Разделы

Аффилиация

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