English
The Jacobi-type identity for triple cross products yields a relation among u⊗v⊗w bracketing.
Русский
Идентичность Якоби для тройственных произведений даёт соотношение между скобками.
LaTeX
$$$u \\times (v \\times w) - (u \\times v) \\times w = - (v \\times (u \\times w))$$$
Lean4
/-- The three-dimensional vectors together with the operations + and ⨯₃ form a Lie ring.
Note we do not make this an instance as a conflicting one already exists
via `LieRing.ofAssociativeRing`. -/
def lieRing : LieRing (Fin 3 → R) :=
{ Pi.addCommGroup with
bracket := fun u v => u ⨯₃ v
add_lie := LinearMap.map_add₂ _
lie_add := fun _ => LinearMap.map_add _
lie_self := cross_self
leibniz_lie := leibniz_cross }
