conjneg

Mathlib.Algebra.Star.Conjneg

URI: https://scilib.ai/kg/mathlib#conjneg

English

Conjugation-negation mapping converts a function f to x ↦ conj(f(-x)).

Русский

Пусть f: G → R; отображение conjneg отправляет f в x ↦ conj(f(-x)).

LaTeX

$$$\\text{conjneg}(f)(x) = \\overline{f(-x)}$$$

Lean4

/-- Conjugation-negation. Sends `f` to `fun x ↦ conj (f (-x))`. -/
def conjneg (f : G → R) : G → R :=
  conj fun x ↦ f (-x)

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

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

Разделы

Аффилиация

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