Theorems · Theorem · linear algebra

jacobi_cross

∀ {R : Type u_1} [inst : CommRing R] (u v w : Fin 3 → R),
  (crossProduct u) ((crossProduct v) w) + (crossProduct v) ((crossProduct w) u) +
      (crossProduct w) ((crossProduct u) v) =
    0

Jacobi identity: For a cross product of three vectors, their sum over the three even permutations is equal to the zero vector.

Defined in

Mathlib.LinearAlgebra.CrossProduct

Cited by

0 results in Mathlib

Foundations

Depth 41 from the axioms · uses propext, Quot.sound

Assumes

CommRing