norm_withLpEquiv_crossProduct — Mathlib

English

The same Lp cross product norm formula holds with the symmetric cross product variant.

Русский

Та же формула норм крок-продукта в варианте симметричной операции crossProduct.

LaTeX

$$‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm (a ⨯₃ b)‖ = ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm a‖ ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm b‖ sin(angle ((WithLp.equiv 2 (Fin 3 → ℝ)).symm a) ((WithLp.equiv 2 (Fin 3 → ℝ)).symm b))$$

Lean4

@[deprecated norm_ofLp_crossProduct (since := "2025-05-04")]
theorem norm_withLpEquiv_crossProduct (a b : EuclideanSpace ℝ (Fin 3)) :
    ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm (WithLp.equiv _ _ a ⨯₃ WithLp.equiv _ _ b)‖ = ‖a‖ * ‖b‖ * sin (angle a b) :=
  norm_ofLp_crossProduct ..

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