English
There is a map for rightAngleRotation under a morphism φ: (Orientation.map (Fin 2) φ.toLinearEquiv o).rightAngleRotation = (φ.symm.trans o.rightAngleRotation).trans φ.
Русский
Сохранение поворота через отображение: (Orientation.map (Fin 2) φ.toLinearEquiv o).rightAngleRotation = (φ.symm.trans o.rightAngleRotation).trans φ.
LaTeX
$$$( Orientation.map (Fin 2) φ.toLinearEquiv o).rightAngleRotation = (φ^{-1}.trans o.rightAngleRotation).trans φ$$$
Lean4
theorem rightAngleRotation_map' {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [Fact (finrank ℝ F = 2)]
(φ : E ≃ₗᵢ[ℝ] F) :
(Orientation.map (Fin 2) φ.toLinearEquiv o).rightAngleRotation = (φ.symm.trans o.rightAngleRotation).trans φ :=
LinearIsometryEquiv.ext <| o.rightAngleRotation_map φ