linearEquiv_det_rotation — Mathlib

English

As a linear equivalence, the rotation by θ has determinant 1: det(o.rotation(θ).toLinearEquiv) = 1.

Русский

Как линейное эквивалентное отображение поворот имеет детерминант 1: det(o.rotation(θ).toLinearEquiv) = 1.

LaTeX

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

Lean4

/-- The determinant of `rotation` (as a linear equiv) is equal to `1`. -/
@[simp]
theorem linearEquiv_det_rotation (θ : Real.Angle) : LinearEquiv.det (o.rotation θ).toLinearEquiv = 1 :=
  Units.ext <| by simpa only [LinearEquiv.coe_det, Units.val_one] using o.det_rotation θ

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