kahler_neg_orientation — Mathlib

English

Flipping orientation negates kahler by complex conjugation: (−o).kahler x y = conj(o.kahler x y).

Русский

Изменение ориентации на противоположную даёт kahler с комплексным сопряжением: (−o).kahler x y = conj(o.kahler x y).

LaTeX

$$(-o).kahler x y = \\overline{o.kahler x y}$$

Lean4

@[simp]
theorem kahler_neg_orientation (x y : E) : (-o).kahler x y = conj (o.kahler x y) := by
  simp [kahler_apply_apply, Complex.conj_ofReal]

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