linearEquiv_det_rotation — Mathlib

English

The determinant of the rotation a (as a linear equivalence) is equal to 1.

Русский

Детерминант вращения a по отношению к линейному эквиваленту равен единице.

LaTeX

$$$\text{LinearEquiv.det}((rotation\;a).toLinearEquiv) = 1$$$

Lean4

/-- The determinant of `rotation` (as a linear equiv) is equal to `1`. -/
@[simp]
theorem linearEquiv_det_rotation (a : Circle) : LinearEquiv.det (rotation a).toLinearEquiv = 1 := by
  rw [← Units.val_inj, LinearEquiv.coe_det, det_rotation, Units.val_one]

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