kahler_comp_linearIsometryEquiv — Mathlib

English

The kahler form is invariant under a positively oriented isometric automorphism: kahler(φx, φy) = kahler(x,y).

Русский

Форма kahler инвариантна относительно положительно ориентированной изометрии: kahler(φx, φy) = kahler(x,y).

LaTeX

$$o.kahler (φ x) (φ y) = o.kahler x y$$

Lean4

/-- The bilinear map `kahler` is invariant under pullback by a positively-oriented isometric
automorphism. -/
theorem kahler_comp_linearIsometryEquiv (φ : E ≃ₗᵢ[ℝ] E) (hφ : 0 < LinearMap.det (φ.toLinearEquiv : E →ₗ[ℝ] E))
    (x y : E) : o.kahler (φ x) (φ y) = o.kahler x y := by
  simp [kahler_apply_apply, o.areaForm_comp_linearIsometryEquiv φ hφ]

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