English
The rotation by θ has the standard 2×2 matrix representation in the right-angle basis: R(θ) = [ [cos θ, −sin θ], [sin θ, cos θ] ].
Русский
Поворот на θ имеет стандартное представление в виде матрицы 2×2: R(θ) = [ [cos θ, −sin θ], [sin θ, cos θ] ].
LaTeX
$$$ (o.rotation(\theta)).toLinearMap = \mathrm{Matrix.toLin}(o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx) \begin{pmatrix} \cos\theta & -\sin\theta \\ \sin\theta & \cos\theta \end{pmatrix} $$$
Lean4
theorem rotation_eq_matrix_toLin (θ : Real.Angle) {x : V} (hx : x ≠ 0) :
(o.rotation θ).toLinearMap =
Matrix.toLin (o.basisRightAngleRotation x hx) (o.basisRightAngleRotation x hx) !![θ.cos, -θ.sin; θ.sin, θ.cos] :=
by
apply (o.basisRightAngleRotation x hx).ext
intro i
fin_cases i
· rw [Matrix.toLin_self]
simp [rotation_apply, Fin.sum_univ_succ]
· rw [Matrix.toLin_self]
simp [rotation_apply, Fin.sum_univ_succ, add_comm]
