inner_smul_rotation_pi_div_two_smul_left

English

The inner product between multiple of a vector and multiple of its π/2 rotation is zero.

Русский

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

LaTeX

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

Lean4

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

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