English
There exists a linear isometry rotating by a given oriented angle in the 2-dimensional setting that respects the real inner product.
Русский
Существует линейная изометрия, совершающая вращение на заданный ориентированный угол в двумерной пространстве и сохраняющая скалярное произведение.
LaTeX
$$$\text{rotationAux}: \mathbb{R}\text{-Angle} \to \text{Isom}_{\mathbb{R}}(V)\; (V\cong\mathbb{R}^2)$$$
Lean4
/-- Auxiliary construction to build a rotation by the oriented angle `θ`. -/
def rotationAux (θ : Real.Angle) : V →ₗᵢ[ℝ] V :=
LinearMap.isometryOfInner
(Real.Angle.cos θ • LinearMap.id + Real.Angle.sin θ • (LinearIsometryEquiv.toLinearEquiv J).toLinearMap)
(by
intro x y
simp only [RCLike.conj_to_real, id, LinearMap.smul_apply, LinearMap.add_apply, LinearMap.id_coe,
LinearEquiv.coe_coe, LinearIsometryEquiv.coe_toLinearEquiv, Orientation.areaForm_rightAngleRotation_left,
Orientation.inner_rightAngleRotation_left, Orientation.inner_rightAngleRotation_right, inner_add_left,
inner_smul_left, inner_add_right, inner_smul_right]
linear_combination ⟪x, y⟫ * θ.cos_sq_add_sin_sq)
