mk_eq_mk_iff_crossProduct_eq_zero

English

For nonzero v,w in Fin 3 → F, the equality mk F v hv = mk F w hw holds iff crossProduct v w = 0.

Русский

Для ненулевых векторов v и w из Fin 3 → F равенство mk F v hv = mk F w hw эквивалентно crossProduct v w = 0.

LaTeX

$$$\\text{mk}(F,v,hv) = \\text{mk}(F,w,hw) \\iff \\text{crossProduct}(v,w) = 0$$$

Lean4

theorem mk_eq_mk_iff_crossProduct_eq_zero {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) :
    mk F v hv = mk F w hw ↔ crossProduct v w = 0 := by
  rw [← not_iff_not, mk_eq_mk_iff', not_exists, ← LinearIndependent.pair_iff' hw, ←
    crossProduct_ne_zero_iff_linearIndependent, ← cross_anticomm, neg_ne_zero]

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