cross_comm — Mathlib

English

If mk F v hv ≠ mk F w hw, then cross (mk F v hv) (mk F w hw) equals mk F (crossProduct v w) h, where h is a witness to nonzero crossProduct.

Русский

Если mk F v hv ≠ mk F w hw, то cross(...) = mk F (crossProduct v w) h, где h — доказательство ненулевого crossProduct.

LaTeX

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

Lean4

theorem cross_comm (v w : ℙ F (Fin 3 → F)) : cross v w = cross w v :=
  by
  rcases eq_or_ne v w with rfl | h
  · rfl
  ·
    induction v with
    | h v hv =>
      induction w with
      | h w hw =>
        rw [cross_mk_of_ne hv hw h, cross_mk_of_ne hw hv h.symm, mk_eq_mk_iff_crossProduct_eq_zero, ←
          cross_anticomm v w, map_neg, _root_.cross_self, neg_zero]

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