det_rotation — Mathlib

English

The determinant of the rotation map is 1 for every θ: det(o.rotation(θ).toLinearMap) = 1.

Русский

Детерминант отображения поворота равен 1 при любом θ: det(o.rotation(θ).toLinearMap) = 1.

LaTeX

$$$ \det\big( o.rotation(\theta).toLinearMap \big) = 1 $$$

Lean4

/-- The determinant of `rotation` (as a linear map) is equal to `1`. -/
@[simp]
theorem det_rotation (θ : Real.Angle) : LinearMap.det (o.rotation θ).toLinearMap = 1 :=
  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)
  rw [o.rotation_eq_matrix_toLin θ hx]
  simpa [sq] using θ.cos_sq_add_sin_sq

Похожие утверждения