Cayley Dickson

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

TheoremArtin's theorem for the double of the quaternions#

the subalgebra generated by two elements x and y is associative.

TauCeti.CayleyDickson.mul_assoc_of_mem_adjoin.{u_1} {R : Type u_1} [CommRing R]
  {x y a b c : TauCeti.CayleyDickson (Quaternion R)} (ha : a ∈ NonUnitalAlgebra.adjoin R {1, x, y})
  (hb : b ∈ NonUnitalAlgebra.adjoin R {1, x, y}) (hc : c ∈ NonUnitalAlgebra.adjoin R {1, x, y}) :
  a * b * c = a * (b * c)
Lean

Formalized in Tau Ceti as TauCeti.CayleyDickson.mul_assoc_of_mem_adjoin.

Sources
LeanTauCeti.CayleyDickson.mul_assoc_of_mem_adjoin

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

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

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

Formalized in Tau Ceti as TauCeti.CayleyDickson.moufang_left.

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

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

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

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

Formalized in Tau Ceti as TauCeti.CayleyDickson.moufang_middle.

Sources
LeanTauCeti.CayleyDickson.moufang_middle

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

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

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

Formalized in Tau Ceti as TauCeti.CayleyDickson.moufang_right.

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

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.