English
Any orientation-preserving linear isometry is a rotation.
Русский
Любой линейный изометрический гомоморфизм, сохраняющий ориентацию, является поворотом.
LaTeX
$$∃ θ : Real.Angle, f = o.rotation θ$$
Lean4
/-- Any linear isometric equivalence in `V` with positive determinant is `rotation`. -/
theorem exists_linearIsometryEquiv_eq_of_det_pos {f : V ≃ₗᵢ[ℝ] V}
(hd : 0 < LinearMap.det (f.toLinearEquiv : V →ₗ[ℝ] V)) : ∃ θ : Real.Angle, f = o.rotation θ :=
by
haveI : Nontrivial V := nontrivial_of_finrank_eq_succ (@Fact.out (finrank ℝ V = 2) _)
obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V)
use o.oangle x (f x)
apply LinearIsometryEquiv.toLinearEquiv_injective
apply LinearEquiv.toLinearMap_injective
apply (o.basisRightAngleRotation x hx).ext
intro i
symm
fin_cases i
· simp
have : o.oangle (J x) (f (J x)) = o.oangle x (f x) := by
simp only [oangle, o.linearIsometryEquiv_comp_rightAngleRotation f hd, o.kahler_comp_rightAngleRotation]
simp [← this]
