conjneg_add

Mathlib.Algebra.Star.Conjneg

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

English

conjneg distributes over addition.

Русский

conjneg распределяется по сложению.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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