cross_self — Mathlib

English

In the projective space, the cross of a point with itself equals the point itself: cross(v,v)=v.

Русский

В проективном пространстве пересечение с самим собой сохраняет точку: cross(v,v)=v.

LaTeX

$$$\\text{cross}(v,v) = v$$$

Lean4

theorem cross_self (v : ℙ F (Fin 3 → F)) : cross v v = v := by
  induction v with
  | h v hv =>
    rw [cross_mk_of_cross_eq_zero]
    rw [← mk_eq_mk_iff_crossProduct_eq_zero hv]

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