inner_smul_rotation_pi_div_two_right

English

The angle between nonzero x and y is θ iff y equals the rotation of x by θ scaled by the norms, or θ = 0 with a zero vector.

Русский

Угол между не нулевыми x и y равен θ тогда и только тогда, когда y равен повороту x на θ, масштабированный нормами, либо θ = 0 и один из векторов нулевой.

LaTeX

$$o.oangle x y = θ ↔ (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r > 0, y = r • o.rotation θ x) ∨ (θ = 0 ∧ (x = 0 ∨ y = 0))$$

Lean4

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

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