rotation_zero — Mathlib

English

Rotation by zero is the identity map: o.rotation(0) = identity linear isometry.

Русский

Поворт на ноль дает тождественное отображение: o.rotation(0) = тождественная линейная изометрия.

LaTeX

$$$ o.rotation(0) = \mathrm{refl} \!\_2 \quad\text{(identity linear isometry)} $$$

Lean4

/-- Rotation by 0 is the identity. -/
@[simp]
theorem rotation_zero : o.rotation 0 = LinearIsometryEquiv.refl ℝ V := by ext; simp [rotation]

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