inner_rotation_pi_div_two_left — Mathlib

English

The inner product between a vector and its image under a π/2 rotation left is zero.

Русский

Скалярное произведение вектора и его образа после поворота на π/2 слева равно нулю.

LaTeX

$$⟪x, o.rotation(π/2) x⟫ = 0$$

Lean4

/-- The inner product between a `π / 2` rotation of a vector and that vector is zero. -/
@[simp]
theorem inner_rotation_pi_div_two_left (x : V) : ⟪o.rotation (π / 2 : ℝ) x, x⟫ = 0 := by
  rw [rotation_pi_div_two, inner_rightAngleRotation_self]

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