cross_orthogonal_left — Mathlib

English

For v,w in projective plane, (v cross w) is orthogonal to v whenever v ≠ w.

Русский

Для любых v,w в проективной плоскости, если v ≠ w, то (v × w) ортогонально v.

LaTeX

$$$(v\\times w)\\ \\perp\\ v$ при $v \\neq w$$$

Lean4

theorem cross_orthogonal_left {v w : ℙ F (Fin 3 → F)} (h : v ≠ w) : (cross v w).orthogonal v := by
  induction v with
  | h v hv =>
    induction w with
    | h w hw => rw [cross_mk_of_ne hv hw h, orthogonal_mk, dotProduct_comm, dot_self_cross]

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