inner_rotation_pi_div_two_left_smul

English

The inner product of x with a real multiple of a π/2 rotation of x is zero.

Русский

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

LaTeX

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

Lean4

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

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