English
There is a rotation by any real angle θ, realized as a real-linear isometry o.rotation(θ) : V ≃ℝ V.
Русский
Существует поворот на любой угол θ в реальном виде: o.rotation(θ) — это линейно-изометричное отображение V в V.
LaTeX
$$$ o.rotation(\theta) : V \to V \quad\text{is a real-linear isometry with } x \mapsto \cos\theta\, x + \sin\theta\, Jx. $$$$
Lean4
/-- A rotation by the oriented angle `θ`. -/
def rotation (θ : Real.Angle) : V ≃ₗᵢ[ℝ] V :=
LinearIsometryEquiv.ofLinearIsometry (o.rotationAux θ)
(Real.Angle.cos θ • LinearMap.id - Real.Angle.sin θ • (LinearIsometryEquiv.toLinearEquiv J).toLinearMap)
(by
ext x
convert congr_arg (fun t : ℝ => t • x) θ.cos_sq_add_sin_sq using 1
· simp only [o.rightAngleRotation_rightAngleRotation, o.rotationAux_apply, Function.comp_apply, id,
LinearEquiv.coe_coe, LinearIsometry.coe_toLinearMap, LinearIsometryEquiv.coe_toLinearEquiv, map_smul, map_sub,
LinearMap.coe_comp, LinearMap.id_coe, LinearMap.smul_apply, LinearMap.sub_apply]
module
· simp)
(by
ext x
convert congr_arg (fun t : ℝ => t • x) θ.cos_sq_add_sin_sq using 1
· simp only [o.rightAngleRotation_rightAngleRotation, o.rotationAux_apply, Function.comp_apply, id,
LinearEquiv.coe_coe, LinearIsometry.coe_toLinearMap, LinearIsometryEquiv.coe_toLinearEquiv, map_add, map_smul,
LinearMap.coe_comp, LinearMap.id_coe, LinearMap.smul_apply, LinearMap.sub_apply]
module
· simp)
