norm_withLpEquiv_symm_crossProduct

English

The symmetric cross product norm identity with equivalence maps.

Русский

Симметричная формула нормы 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

/-- 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. -/
@[deprecated norm_toLp_symm_crossProduct (since := "2025-05-04")]
theorem norm_withLpEquiv_symm_crossProduct (a b : Fin 3 → ℝ) :
    ‖(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)) :=
  norm_toLp_symm_crossProduct ..

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