kahler_swap — Mathlib

English

Swapping the arguments reflects complex conjugation: kahler x y = conj (kahler y x).

Русский

Перестановка аргументов соответствует комплексному сопряжению: kahler x y = conj (kahler y x).

LaTeX

$$kahler\\_swap (x,y) : o.kahler x y = \\overline{ o.kahler y x }$$

Lean4

theorem kahler_swap (x y : E) : o.kahler x y = conj (o.kahler y x) :=
  by
  simp only [kahler_apply_apply]
  rw [real_inner_comm, areaForm_swap]
  simp [Complex.conj_ofReal]

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