rotationOf — Mathlib

English

The operator rotationOf takes a linear isometry and returns the corresponding unit-circle element; specifically, rotationOf(rotation a) = a.

Русский

Оператор rotationOf сопоставляет изометрии на единичную окружность; в частности, rotationOf(rotation(a)) = a.

LaTeX

$$$rotationOf\,(rotation\;a) = a$$$

Lean4

/-- Takes an element of `ℂ ≃ₗᵢ[ℝ] ℂ` and checks if it is a rotation, returns an element of the
unit circle. -/
@[simps]
def rotationOf (e : ℂ ≃ₗᵢ[ℝ] ℂ) : Circle :=
  ⟨e 1 / ‖e 1‖, by simp [Submonoid.unitSphere]⟩

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