rotation_pi_div_two — Mathlib

English

Rotating by θ1 and then by θ2 equals a rotation by θ1 + θ2: o.rotation(θ1) ∘ o.rotation(θ2) = o.rotation(θ1 + θ2).

Русский

Поворот на θ1, затем на θ2 эквивалентен повороту на θ1 + θ2: o.rotation(θ1) ∘ o.rotation(θ2) = o.rotation(θ1 + θ2).

LaTeX

$$$ o.rotation(\theta_1) \circ o.rotation(\theta_2) = o.rotation(\theta_1 + \theta_2) $$$

Lean4

/-- Rotation by π / 2 is the "right-angle-rotation" map `J`. -/
theorem rotation_pi_div_two : o.rotation (π / 2 : ℝ) = J :=
  by
  ext x
  simp [rotation]

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