conj_mul

Mathlib.Analysis.Complex.UnitDisc.Basic

URI: https://scilib.ai/kg/mathlib#Complex.UnitDisc.conj_mul

English

Conjugation preserves multiplication: (z w).conj = z.conj w.conj.

Русский

Сопряжение сохраняет умножение: (z w).conj = z.conj w.conj.

LaTeX

$$$\forall z,w \in \mathbb{D}, (z w).conj = z.conj w.conj$$$

Lean4

@[simp]
theorem conj_mul (z w : 𝔻) : (z * w).conj = z.conj * w.conj :=
  Subtype.ext <| map_mul _ _ _

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

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

Разделы

Аффилиация

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