Octonion

Results named in Tau Ceti's TauCeti.Algebra.Octonion modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe left Moufang identity (TauCeti.Octonion.moufang_left)#

(z * x * z) * y = z * (x * (z * y)).

TauCeti.Octonion.moufang_left.{u_1} {R : Type u_1} [CommRing R] (x y z : TauCeti.Octonion R) :
  z * x * z * y = z * (x * (z * y))
Lean

Formalized in Tau Ceti as TauCeti.Octonion.moufang_left.

Sources
LeanTauCeti.Octonion.moufang_left
Used by 1
Used byThe right Moufang identity (TauCeti.Octonion.moufang_right)

TheoremThe middle Moufang identity (TauCeti.Octonion.moufang_middle)#

(z * x) * (y * z) = (z * (x * y)) * z.

TauCeti.Octonion.moufang_middle.{u_1} {R : Type u_1} [CommRing R] (x y z : TauCeti.Octonion R) :
  z * x * (y * z) = z * (x * y) * z
Lean

Formalized in Tau Ceti as TauCeti.Octonion.moufang_middle.

Sources
LeanTauCeti.Octonion.moufang_middle

TheoremThe right Moufang identity (TauCeti.Octonion.moufang_right)#

x * (z * y * z) = ((x * z) * y) * z.

TauCeti.Octonion.moufang_right.{u_1} {R : Type u_1} [CommRing R] (x y z : TauCeti.Octonion R) :
  x * (z * y * z) = x * z * y * z
Lean

Formalized in Tau Ceti as TauCeti.Octonion.moufang_right.

Sources
LeanTauCeti.Octonion.moufang_right
Uses 1
Proof usesThe left Moufang identity (TauCeti.Octonion.moufang_left)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.