norm_toLp_symm_crossProduct — Mathlib

English

For a,b ∈ Fin 3 → ℝ, the symmetric cross product norm formula holds.

Русский

Для a,b ∈ Fin 3 → ℝ, справедлива формула симметричной нормы crossProduct.

LaTeX

$$‖toLp 2 (a ⨯₃ b)‖ = ‖toLp 2 a‖ ‖toLp 2 b‖ sin(angle (toLp 2 a) (toLp 2 b))$$

Lean4

/-- The L2 norm of the cross product of two real vectors (of type `Fin 3 → R`) equals the product
of their individual L2 norms times the sine of the angle between them. -/
theorem norm_toLp_symm_crossProduct (a b : Fin 3 → ℝ) :
    ‖toLp 2 (a ⨯₃ b)‖ = ‖toLp 2 a‖ * ‖toLp 2 b‖ * sin (angle (toLp 2 a) (toLp 2 b)) := by
  simp [← norm_ofLp_crossProduct (toLp 2 a) (toLp 2 b)]

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