kahler_comp_rightAngleRotation — Mathlib

English

Kähler is preserved under pullback by a linear isometry between oriented 2D spaces: kahler(φx, φy) = kahler(x,y).

Русский

Kähler сохраняется при вытягивании по линейному изоморфизму между ориентированными двумерными пространствами: kahler(φx, φy) = kahler(x,y).

LaTeX

$$kahler\\_comp\\_linearIsometryEquiv (φ) (x,y) : o.kahler (φ x) (φ y) = o.kahler x y$$

Lean4

theorem kahler_comp_rightAngleRotation (x y : E) : o.kahler (J x) (J y) = o.kahler x y :=
  by
  simp only [kahler_rightAngleRotation_left, kahler_rightAngleRotation_right]
  linear_combination -o.kahler x y * Complex.I_sq

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