linearIsometryEquiv_comp_rightAngleRotation

English

This is the same skew-adjoint property as in 52067: ⟪x, J y⟫ = −⟪J x, y⟫.

Русский

То же свойство кососимметричности: ⟪x, J y⟫ = −⟪J x, y⟫.

LaTeX

$$$\\\\langle x, J y\\\\rangle = -\\\\langle J x, y\\\\rangle$$$

Lean4

/-- `J` commutes with any positively-oriented isometric automorphism. -/
theorem linearIsometryEquiv_comp_rightAngleRotation (φ : E ≃ₗᵢ[ℝ] E)
    (hφ : 0 < LinearMap.det (φ.toLinearEquiv : E →ₗ[ℝ] E)) (x : E) : φ (J x) = J (φ x) :=
  by
  convert (o.rightAngleRotation_map φ (φ x)).symm
  · simp
  · symm
    rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
    rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]

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