conjneg_mul

Mathlib.Algebra.Star.Conjneg

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

English

conjneg distributes over multiplication.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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