conjneg_conjneg

Mathlib.Algebra.Star.Conjneg

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

English

Applying conjneg twice yields the original function.

Русский

Применение conjneg дважды возвращает исходную функцию.

LaTeX

$$$\\text{conjneg}(\\text{conjneg}(f)) = f$$$

Lean4

@[simp]
theorem conjneg_conjneg (f : G → R) : conjneg (conjneg f) = f := by ext; simp

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

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

Разделы

Аффилиация

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