Theorems · Theorem · linear algebra

cross_apply

∀ {R : Type u_1} [inst : CommRing R] (a b : Fin 3 → R),
  (crossProduct a) b = ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]

Defined in

Mathlib.LinearAlgebra.CrossProduct

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRing