linearIsometryEquiv_comp_rightAngleRotation'

English

J commutes with any positively oriented isometric automorphism φ: φ(J x) = J(φ x) whenever det φ > 0.

Русский

J коммутирует с любым положительно ориентированным изометрическим автоморфизмом φ: φ(J x) = J(φ x) при det φ > 0.

LaTeX

$$$\\\\phi \\\\circ J = J \\\\circ \\\\phi$ for 0 < det(φ.toLinearEquiv).$$

Lean4

/-- `J` commutes with any positively-oriented isometric automorphism. -/
theorem linearIsometryEquiv_comp_rightAngleRotation' (φ : E ≃ₗᵢ[ℝ] E)
    (hφ : 0 < LinearMap.det (φ.toLinearEquiv : E →ₗ[ℝ] E)) : LinearIsometryEquiv.trans J φ = φ.trans J :=
  LinearIsometryEquiv.ext <| o.linearIsometryEquiv_comp_rightAngleRotation φ hφ

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