rotationOf_rotation

Mathlib.Analysis.Complex.Isometry

URI: https://scilib.ai/kg/mathlib#rotationOf_rotation

English

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

Русский

Детерминант вращения a равно 1.

LaTeX

$$$\det\bigl((rotation\,a)^{\to\;\text{LinearMap}}\bigr) = 1$$$

Lean4

@[simp]
theorem rotationOf_rotation (a : Circle) : rotationOf (rotation a) = a :=
  Subtype.ext <| by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru