Quaternions

In this file we define quaternions ℍ[R] over a commutative ring R, and define some algebraic structures on ℍ[R].

Main definitions

• QuaternionAlgebra R a b c, ℍ[R, a, b, c] : [Bourbaki, Algebra I][bourbaki1989] with coefficients a, b, c (Many other references such as Wikipedia assume $\operatorname{char} R ≠ 2$ therefore one can complete the square and WLOG assume $b = 0$.)
• Quaternion R, ℍ[R] : the space of quaternions, a.k.a. QuaternionAlgebra R (-1) (0) (-1);
• Quaternion.normSq : square of the norm of a quaternion;

We also define the following algebraic structures on ℍ[R]:

• Ring ℍ[R, a, b, c], StarRing ℍ[R, a, b, c], and Algebra R ℍ[R, a, b, c] : for any commutative ring R;
• Ring ℍ[R], StarRing ℍ[R], and Algebra R ℍ[R] : for any commutative ring R;
• IsDomain ℍ[R] : for a linear ordered commutative ring R;
• DivisionRing ℍ[R] : for a linear ordered field R.

Notation

The following notation is available with open Quaternion or open scoped Quaternion.

• ℍ[R,c₁,c₂,c₃] : QuaternionAlgebra R c₁ c₂ c₃
• ℍ[R,c₁,c₂] : QuaternionAlgebra R c₁ 0 c₂
• ℍ[R] : quaternions over R.

Implementation notes

We define quaternions over any ring R, not just ℝ to be able to deal with, e.g., integer or rational quaternions without using real numbers. In particular, all definitions in this file are computable.

Tags

quaternion

structure QuaternionAlgebra (R : Type u_1) (a b c : R) : Type u_1

Quaternion algebra over a type with fixed coefficients where $i^2 = a + bi$ and $j^2 = c$, denoted as ℍ[R,a,b]. Implemented as a structure with four fields: re, imI, imJ, and imK.

• re : R

  Real part of a quaternion.

• imI : R

  First imaginary part (i) of a quaternion.

• imJ : R

  Second imaginary part (j) of a quaternion.

• imK : R

  Third imaginary part (k) of a quaternion.

theorem QuaternionAlgebra.ext {R : Type u_1} {a b c : R} {x y : QuaternionAlgebra R a b c} (re : x.re = y.re) (imI : x.imI = y.imI) (imJ : x.imJ = y.imJ) (imK : x.imK = y.imK) : x = y

theorem QuaternionAlgebra.ext_iff {R : Type u_1} {a b c : R} {x y : QuaternionAlgebra R a b c} : x = y ↔ x.re = y.re ∧ x.imI = y.imI ∧ x.imJ = y.imJ ∧ x.imK = y.imK

def Quaternion.«termℍ[_,_,_,_]» : Lean.ParserDescr

Quaternion algebra over a type with fixed coefficients where $i^2 = a + bi$ and $j^2 = c$, denoted as ℍ[R,a,b]. Implemented as a structure with four fields: re, imI, imJ, and imK.

Equations

• One or more equations did not get rendered due to their size.

def Quaternion.«termℍ[_,_,_]» : Lean.ParserDescr

Quaternion algebra over a type with fixed coefficients where $i^2 = a + bi$ and $j^2 = c$, denoted as ℍ[R,a,b]. Implemented as a structure with four fields: re, imI, imJ, and imK.

Equations

• One or more equations did not get rendered due to their size.

def QuaternionAlgebra.equivProd {R : Type u_1} (c₁ c₂ c₃ : R) : QuaternionAlgebra R c₁ c₂ c₃ ≃ R × R × R × R

The equivalence between a quaternion algebra over R and R × R × R × R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuaternionAlgebra.equivProd_apply {R : Type u_1} (c₁ c₂ c₃ : R) (a : QuaternionAlgebra R c₁ c₂ c₃) : (equivProd c₁ c₂ c₃) a = (a.re, a.imI, a.imJ, a.imK)

@[simp]

theorem QuaternionAlgebra.imJ_equivProd_symm_apply {R : Type u_1} (c₁ c₂ c₃ : R) (a : R × R × R × R) : ((equivProd c₁ c₂ c₃).symm a).imJ = a.2.2.1

@[simp]

theorem QuaternionAlgebra.re_equivProd_symm_apply {R : Type u_1} (c₁ c₂ c₃ : R) (a : R × R × R × R) : ((equivProd c₁ c₂ c₃).symm a).re = a.1

@[simp]

theorem QuaternionAlgebra.imK_equivProd_symm_apply {R : Type u_1} (c₁ c₂ c₃ : R) (a : R × R × R × R) : ((equivProd c₁ c₂ c₃).symm a).imK = a.2.2.2

@[simp]

theorem QuaternionAlgebra.imI_equivProd_symm_apply {R : Type u_1} (c₁ c₂ c₃ : R) (a : R × R × R × R) : ((equivProd c₁ c₂ c₃).symm a).imI = a.2.1

def QuaternionAlgebra.equivTuple {R : Type u_1} (c₁ c₂ c₃ : R) : QuaternionAlgebra R c₁ c₂ c₃ ≃ (Fin 4 → R)

The equivalence between a quaternion algebra over R and Fin 4 → R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuaternionAlgebra.equivTuple_symm_apply {R : Type u_1} (c₁ c₂ c₃ : R) (a : Fin 4 → R) : (equivTuple c₁ c₂ c₃).symm a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }

@[simp]

theorem QuaternionAlgebra.equivTuple_apply {R : Type u_1} (c₁ c₂ c₃ : R) (x : QuaternionAlgebra R c₁ c₂ c₃) : (equivTuple c₁ c₂ c₃) x = ![x.re, x.imI, x.imJ, x.imK]

@[simp]

theorem QuaternionAlgebra.mk.eta {R : Type u_1} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) : { re := a.re, imI := a.imI, imJ := a.imJ, imK := a.imK } = a

instance QuaternionAlgebra.instSubsingleton {R : Type u_3} {c₁ c₂ c₃ : R} [Subsingleton R] : Subsingleton (QuaternionAlgebra R c₁ c₂ c₃)

instance QuaternionAlgebra.instNontrivial {R : Type u_3} {c₁ c₂ c₃ : R} [Nontrivial R] : Nontrivial (QuaternionAlgebra R c₁ c₂ c₃)

def QuaternionAlgebra.im {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] (x : QuaternionAlgebra R c₁ c₂ c₃) : QuaternionAlgebra R c₁ c₂ c₃

The imaginary part of a quaternion.

Note that unless c₂ = 0, this definition is not particularly well-behaved; for instance, QuaternionAlgebra.star_im only says that the star of an imaginary quaternion is imaginary under this condition.

Equations

• x.im = { re := 0, imI := x.imI, imJ := x.imJ, imK := x.imK }

@[simp]

theorem QuaternionAlgebra.re_im {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [Zero R] : a.im.re = 0

@[simp]

theorem QuaternionAlgebra.imI_im {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [Zero R] : a.im.imI = a.imI

@[simp]

theorem QuaternionAlgebra.imJ_im {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [Zero R] : a.im.imJ = a.imJ

@[simp]

theorem QuaternionAlgebra.imK_im {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [Zero R] : a.im.imK = a.imK

@[simp]

theorem QuaternionAlgebra.im_idem {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [Zero R] : a.im.im = a.im

def QuaternionAlgebra.coe {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] (x : R) : QuaternionAlgebra R c₁ c₂ c₃

Coercion R → ℍ[R,c₁,c₂,c₃].

Equations

• ↑x = { re := x, imI := 0, imJ := 0, imK := 0 }

@[instance_reducible]

instance QuaternionAlgebra.instCoeTC {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] : CoeTC R (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• QuaternionAlgebra.instCoeTC = { coe := QuaternionAlgebra.coe }

@[simp]

theorem QuaternionAlgebra.re_coe {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [Zero R] : (↑x).re = x

@[simp]

theorem QuaternionAlgebra.imI_coe {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [Zero R] : (↑x).imI = 0

@[simp]

theorem QuaternionAlgebra.imJ_coe {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [Zero R] : (↑x).imJ = 0

@[simp]

theorem QuaternionAlgebra.imK_coe {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [Zero R] : (↑x).imK = 0

theorem QuaternionAlgebra.coe_injective {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] : Function.Injective coe

@[simp]

theorem QuaternionAlgebra.coe_inj {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] {x y : R} : ↑x = ↑y ↔ x = y

@[instance_reducible]

instance QuaternionAlgebra.instZero {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] : Zero (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• QuaternionAlgebra.instZero = { zero := { re := 0, imI := 0, imJ := 0, imK := 0 } }

@[simp]

theorem QuaternionAlgebra.imJ_zero {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] : imJ 0 = 0

@[simp]

theorem QuaternionAlgebra.imI_zero {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] : imI 0 = 0

@[simp]

theorem QuaternionAlgebra.re_zero {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] : re 0 = 0

@[simp]

theorem QuaternionAlgebra.imK_zero {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] : imK 0 = 0

theorem QuaternionAlgebra.im_zero {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] : im 0 = 0

@[simp]

theorem QuaternionAlgebra.coe_zero {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] : ↑0 = 0

@[instance_reducible]

instance QuaternionAlgebra.instInhabited {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] : Inhabited (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• QuaternionAlgebra.instInhabited = { default := 0 }

@[instance_reducible]

instance QuaternionAlgebra.instOne {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] [One R] : One (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• QuaternionAlgebra.instOne = { one := { re := 1, imI := 0, imJ := 0, imK := 0 } }

@[simp]

theorem QuaternionAlgebra.imK_one {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] [One R] : imK 1 = 0

@[simp]

theorem QuaternionAlgebra.imJ_one {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] [One R] : imJ 1 = 0

@[simp]

theorem QuaternionAlgebra.imI_one {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] [One R] : imI 1 = 0

@[simp]

theorem QuaternionAlgebra.re_one {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] [One R] : re 1 = 1

theorem QuaternionAlgebra.im_one {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] [One R] : im 1 = 0

@[simp]

theorem QuaternionAlgebra.coe_one {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] [One R] : ↑1 = 1

@[instance_reducible]

instance QuaternionAlgebra.instAdd {R : Type u_3} {c₁ c₂ c₃ : R} [Add R] : Add (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• QuaternionAlgebra.instAdd = { add := fun (a b : QuaternionAlgebra R c₁ c₂ c₃) => { re := a.re + b.re, imI := a.imI + b.imI, imJ := a.imJ + b.imJ, imK := a.imK + b.imK } }

@[simp]

theorem QuaternionAlgebra.imJ_add {R : Type u_3} {c₁ c₂ c₃ : R} [Add R] (a b : QuaternionAlgebra R c₁ c₂ c₃) : (a + b).imJ = a.imJ + b.imJ

@[simp]

theorem QuaternionAlgebra.imI_add {R : Type u_3} {c₁ c₂ c₃ : R} [Add R] (a b : QuaternionAlgebra R c₁ c₂ c₃) : (a + b).imI = a.imI + b.imI

@[simp]

theorem QuaternionAlgebra.re_add {R : Type u_3} {c₁ c₂ c₃ : R} [Add R] (a b : QuaternionAlgebra R c₁ c₂ c₃) : (a + b).re = a.re + b.re

@[simp]

theorem QuaternionAlgebra.imK_add {R : Type u_3} {c₁ c₂ c₃ : R} [Add R] (a b : QuaternionAlgebra R c₁ c₂ c₃) : (a + b).imK = a.imK + b.imK

@[simp]

theorem QuaternionAlgebra.mk_add_mk {R : Type u_3} {c₁ c₂ c₃ : R} [Add R] (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) : { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } + { re := b₁, imI := b₂, imJ := b₃, imK := b₄ } = { re := a₁ + b₁, imI := a₂ + b₂, imJ := a₃ + b₃, imK := a₄ + b₄ }

def QuaternionAlgebra.addEquivTuple {R : Type u_3} [Add R] (c₁ c₂ c₃ : R) : QuaternionAlgebra R c₁ c₂ c₃ ≃+ (Fin 4 → R)

The additive equivalence between a quaternion algebra over R and Fin 4 → R.

Equations

• QuaternionAlgebra.addEquivTuple c₁ c₂ c₃ = (QuaternionAlgebra.equivTuple c₁ c₂ c₃).addEquiv

@[simp]

theorem QuaternionAlgebra.coe_addEquivTuple {R : Type u_3} [Add R] (c₁ c₂ c₃ : R) : ⇑(addEquivTuple c₁ c₂ c₃) = ⇑(equivTuple c₁ c₂ c₃)

@[simp]

theorem QuaternionAlgebra.coe_symm_addEquivTuple {R : Type u_3} [Add R] (c₁ c₂ c₃ : R) : ⇑(addEquivTuple c₁ c₂ c₃).symm = ⇑(equivTuple c₁ c₂ c₃).symm

def QuaternionAlgebra.addEquivProd {R : Type u_3} [Add R] (c₁ c₂ c₃ : R) : QuaternionAlgebra R c₁ c₂ c₃ ≃+ R × R × R × R

The additive equivalence between a quaternion algebra over R and R × R × R × R.

Equations

• QuaternionAlgebra.addEquivProd c₁ c₂ c₃ = (QuaternionAlgebra.equivProd c₁ c₂ c₃).addEquiv

@[simp]

theorem QuaternionAlgebra.coe_addEquivProd {R : Type u_3} [Add R] (c₁ c₂ c₃ : R) : ⇑(addEquivProd c₁ c₂ c₃) = ⇑(equivProd c₁ c₂ c₃)

@[simp]

theorem QuaternionAlgebra.coe_symm_addEquivProd {R : Type u_3} [Add R] (c₁ c₂ c₃ : R) : ⇑(addEquivProd c₁ c₂ c₃).symm = ⇑(equivProd c₁ c₂ c₃).symm

@[simp]

theorem QuaternionAlgebra.im_add {R : Type u_3} {c₁ c₂ c₃ : R} (a b : QuaternionAlgebra R c₁ c₂ c₃) [AddZeroClass R] : (a + b).im = a.im + b.im

@[simp]

theorem QuaternionAlgebra.coe_add {R : Type u_3} {c₁ c₂ c₃ : R} (x y : R) [AddZeroClass R] : ↑(x + y) = ↑x + ↑y

@[instance_reducible]

instance QuaternionAlgebra.instNeg {R : Type u_3} {c₁ c₂ c₃ : R} [Neg R] : Neg (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• QuaternionAlgebra.instNeg = { neg := fun (a : QuaternionAlgebra R c₁ c₂ c₃) => { re := -a.re, imI := -a.imI, imJ := -a.imJ, imK := -a.imK } }

@[simp]

theorem QuaternionAlgebra.imJ_neg {R : Type u_3} {c₁ c₂ c₃ : R} [Neg R] (a : QuaternionAlgebra R c₁ c₂ c₃) : (-a).imJ = -a.imJ

@[simp]

theorem QuaternionAlgebra.re_neg {R : Type u_3} {c₁ c₂ c₃ : R} [Neg R] (a : QuaternionAlgebra R c₁ c₂ c₃) : (-a).re = -a.re

@[simp]

theorem QuaternionAlgebra.imK_neg {R : Type u_3} {c₁ c₂ c₃ : R} [Neg R] (a : QuaternionAlgebra R c₁ c₂ c₃) : (-a).imK = -a.imK

@[simp]

theorem QuaternionAlgebra.imI_neg {R : Type u_3} {c₁ c₂ c₃ : R} [Neg R] (a : QuaternionAlgebra R c₁ c₂ c₃) : (-a).imI = -a.imI

@[simp]

theorem QuaternionAlgebra.neg_mk {R : Type u_3} {c₁ c₂ c₃ : R} [Neg R] (a₁ a₂ a₃ a₄ : R) : -{ re := a₁, imI := a₂, imJ := a₃, imK := a₄ } = { re := -a₁, imI := -a₂, imJ := -a₃, imK := -a₄ }

@[simp]

theorem QuaternionAlgebra.im_neg {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [AddGroup R] : (-a).im = -a.im

@[simp]

theorem QuaternionAlgebra.coe_neg {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [AddGroup R] : ↑(-x) = -↑x

@[instance_reducible]

instance QuaternionAlgebra.instSub {R : Type u_3} {c₁ c₂ c₃ : R} [AddGroup R] : Sub (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• QuaternionAlgebra.instSub = { sub := fun (a b : QuaternionAlgebra R c₁ c₂ c₃) => { re := a.re - b.re, imI := a.imI - b.imI, imJ := a.imJ - b.imJ, imK := a.imK - b.imK } }

@[simp]

theorem QuaternionAlgebra.re_sub {R : Type u_3} {c₁ c₂ c₃ : R} [AddGroup R] (a b : QuaternionAlgebra R c₁ c₂ c₃) : (a - b).re = a.re - b.re

@[simp]

theorem QuaternionAlgebra.imK_sub {R : Type u_3} {c₁ c₂ c₃ : R} [AddGroup R] (a b : QuaternionAlgebra R c₁ c₂ c₃) : (a - b).imK = a.imK - b.imK

@[simp]

theorem QuaternionAlgebra.imJ_sub {R : Type u_3} {c₁ c₂ c₃ : R} [AddGroup R] (a b : QuaternionAlgebra R c₁ c₂ c₃) : (a - b).imJ = a.imJ - b.imJ

@[simp]

theorem QuaternionAlgebra.imI_sub {R : Type u_3} {c₁ c₂ c₃ : R} [AddGroup R] (a b : QuaternionAlgebra R c₁ c₂ c₃) : (a - b).imI = a.imI - b.imI

@[simp]

theorem QuaternionAlgebra.im_sub {R : Type u_3} {c₁ c₂ c₃ : R} (a b : QuaternionAlgebra R c₁ c₂ c₃) [AddGroup R] : (a - b).im = a.im - b.im

@[simp]

theorem QuaternionAlgebra.mk_sub_mk {R : Type u_3} {c₁ c₂ c₃ : R} [AddGroup R] (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) : { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } - { re := b₁, imI := b₂, imJ := b₃, imK := b₄ } = { re := a₁ - b₁, imI := a₂ - b₂, imJ := a₃ - b₃, imK := a₄ - b₄ }

@[simp]

theorem QuaternionAlgebra.im_coe {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [AddGroup R] : (↑x).im = 0

@[simp]

theorem QuaternionAlgebra.re_add_im {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [AddGroup R] : ↑a.re + a.im = a

@[simp]

theorem QuaternionAlgebra.sub_im_self {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [AddGroup R] : a - a.im = ↑a.re

@[simp]

theorem QuaternionAlgebra.sub_re_self {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [AddGroup R] : a - ↑a.re = a.im

@[instance_reducible]

instance QuaternionAlgebra.instMul {R : Type u_3} {c₁ c₂ c₃ : R} [Ring R] : Mul (QuaternionAlgebra R c₁ c₂ c₃)

Multiplication is given by

• 1 * x = x * 1 = x;
• i * i = c₁ + c₂ * i;
• j * j = c₃;
• i * j = k, j * i = c₂ * j - k;
• k * k = - c₁ * c₃;
• i * k = c₁ * j + c₂ * k, k * i = -c₁ * j;
• j * k = c₂ * c₃ - c₃ * i, k * j = c₃ * i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuaternionAlgebra.imI_mul {R : Type u_3} {c₁ c₂ c₃ : R} [Ring R] (a b : QuaternionAlgebra R c₁ c₂ c₃) : (a * b).imI = a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI - c₃ * a.imJ * b.imK + c₃ * a.imK * b.imJ

@[simp]

theorem QuaternionAlgebra.imJ_mul {R : Type u_3} {c₁ c₂ c₃ : R} [Ring R] (a b : QuaternionAlgebra R c₁ c₂ c₃) : (a * b).imJ = a.re * b.imJ + c₁ * a.imI * b.imK + a.imJ * b.re + c₂ * a.imJ * b.imI - c₁ * a.imK * b.imI

@[simp]

theorem QuaternionAlgebra.imK_mul {R : Type u_3} {c₁ c₂ c₃ : R} [Ring R] (a b : QuaternionAlgebra R c₁ c₂ c₃) : (a * b).imK = a.re * b.imK + a.imI * b.imJ + c₂ * a.imI * b.imK - a.imJ * b.imI + a.imK * b.re

@[simp]

theorem QuaternionAlgebra.re_mul {R : Type u_3} {c₁ c₂ c₃ : R} [Ring R] (a b : QuaternionAlgebra R c₁ c₂ c₃) : (a * b).re = a.re * b.re + c₁ * a.imI * b.imI + c₃ * a.imJ * b.imJ + c₂ * c₃ * a.imJ * b.imK - c₁ * c₃ * a.imK * b.imK

@[simp]

theorem QuaternionAlgebra.mk_mul_mk {R : Type u_3} {c₁ c₂ c₃ : R} [Ring R] (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) : { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } * { re := b₁, imI := b₂, imJ := b₃, imK := b₄ } = { re := a₁ * b₁ + c₁ * a₂ * b₂ + c₃ * a₃ * b₃ + c₂ * c₃ * a₃ * b₄ - c₁ * c₃ * a₄ * b₄, imI := a₁ * b₂ + a₂ * b₁ + c₂ * a₂ * b₂ - c₃ * a₃ * b₄ + c₃ * a₄ * b₃, imJ := a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ + c₂ * a₃ * b₂ - c₁ * a₄ * b₂, imK := a₁ * b₄ + a₂ * b₃ + c₂ * a₂ * b₄ - a₃ * b₂ + a₄ * b₁ }

@[instance_reducible]

instance QuaternionAlgebra.instSMul {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [SMul S R] : SMul S (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• QuaternionAlgebra.instSMul = { smul := fun (s : S) (a : QuaternionAlgebra R c₁ c₂ c₃) => { re := s • a.re, imI := s • a.imI, imJ := s • a.imJ, imK := s • a.imK } }

@[simp]

theorem QuaternionAlgebra.re_smul {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [SMul S R] (s : S) (a : QuaternionAlgebra R c₁ c₂ c₃) : (s • a).re = s • a.re

@[simp]

theorem QuaternionAlgebra.imJ_smul {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [SMul S R] (s : S) (a : QuaternionAlgebra R c₁ c₂ c₃) : (s • a).imJ = s • a.imJ

@[simp]

theorem QuaternionAlgebra.imI_smul {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [SMul S R] (s : S) (a : QuaternionAlgebra R c₁ c₂ c₃) : (s • a).imI = s • a.imI

@[simp]

theorem QuaternionAlgebra.imK_smul {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [SMul S R] (s : S) (a : QuaternionAlgebra R c₁ c₂ c₃) : (s • a).imK = s • a.imK

instance QuaternionAlgebra.instIsScalarTower {S : Type u_1} {T : Type u_2} {R : Type u_3} {c₁ c₂ c₃ : R} [SMul S R] [SMul T R] [SMul S T] [IsScalarTower S T R] : IsScalarTower S T (QuaternionAlgebra R c₁ c₂ c₃)

instance QuaternionAlgebra.instSMulCommClass {S : Type u_1} {T : Type u_2} {R : Type u_3} {c₁ c₂ c₃ : R} [SMul S R] [SMul T R] [SMulCommClass S T R] : SMulCommClass S T (QuaternionAlgebra R c₁ c₂ c₃)

@[simp]

theorem QuaternionAlgebra.im_smul {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) {S : Type u_4} [CommRing R] [SMulZeroClass S R] (s : S) : (s • a).im = s • a.im

@[simp]

theorem QuaternionAlgebra.smul_mk {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [SMul S R] (s : S) (re im_i im_j im_k : R) : s • { re := re, imI := im_i, imJ := im_j, imK := im_k } = { re := s • re, imI := s • im_i, imJ := s • im_j, imK := s • im_k }

@[instance_reducible]

instance QuaternionAlgebra.instMulAction {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [Monoid S] [MulAction S R] : MulAction S (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• QuaternionAlgebra.instMulAction = Function.Injective.mulAction ⇑(QuaternionAlgebra.equivProd c₁ c₂ c₃) ⋯ ⋯

@[instance_reducible]

instance QuaternionAlgebra.instAddCommGroup {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroup R] : AddCommGroup (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• QuaternionAlgebra.instAddCommGroup = Function.Injective.addCommGroup ⇑(QuaternionAlgebra.equivProd c₁ c₂ c₃) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem QuaternionAlgebra.coe_smul {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [Zero R] [SMulZeroClass S R] (s : S) (r : R) : ↑(s • r) = s • ↑r

@[instance_reducible]

instance QuaternionAlgebra.instDistribMulAction {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [Semiring S] [AddCommGroup R] [DistribMulAction S R] : DistribMulAction S (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• QuaternionAlgebra.instDistribMulAction = Function.Injective.distribMulAction (QuaternionAlgebra.addEquivProd c₁ c₂ c₃).toAddMonoidHom ⋯ ⋯

@[instance_reducible]

instance QuaternionAlgebra.instModule {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [Semiring S] [AddCommGroup R] [Module S R] : Module S (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• QuaternionAlgebra.instModule = Function.Injective.module S (QuaternionAlgebra.addEquivProd c₁ c₂ c₃).toAddMonoidHom ⋯ ⋯

@[instance_reducible]

instance QuaternionAlgebra.instAddCommGroupWithOne {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] : AddCommGroupWithOne (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuaternionAlgebra.re_natCast {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (n : ℕ) : (↑n).re = ↑n

@[simp]

theorem QuaternionAlgebra.imI_natCast {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (n : ℕ) : (↑n).imI = 0

@[simp]

theorem QuaternionAlgebra.imJ_natCast {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (n : ℕ) : (↑n).imJ = 0

@[simp]

theorem QuaternionAlgebra.imK_natCast {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (n : ℕ) : (↑n).imK = 0

@[simp]

theorem QuaternionAlgebra.im_natCast {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (n : ℕ) : (↑n).im = 0

theorem QuaternionAlgebra.coe_natCast {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem QuaternionAlgebra.re_intCast {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (z : ℤ) : (↑z).re = ↑z

theorem QuaternionAlgebra.re_ofNat {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).re = OfNat.ofNat n

theorem QuaternionAlgebra.imI_ofNat {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).imI = 0

theorem QuaternionAlgebra.imJ_ofNat {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).imJ = 0

theorem QuaternionAlgebra.imK_ofNat {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).imK = 0

theorem QuaternionAlgebra.im_ofNat {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).im = 0

@[simp]

theorem QuaternionAlgebra.imI_intCast {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (z : ℤ) : (↑z).imI = 0

@[simp]

theorem QuaternionAlgebra.imJ_intCast {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (z : ℤ) : (↑z).imJ = 0

@[simp]

theorem QuaternionAlgebra.imK_intCast {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (z : ℤ) : (↑z).imK = 0

@[simp]

theorem QuaternionAlgebra.im_intCast {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (z : ℤ) : (↑z).im = 0

theorem QuaternionAlgebra.coe_intCast {R : Type u_3} {c₁ c₂ c₃ : R} [AddCommGroupWithOne R] (z : ℤ) : ↑↑z = ↑z

@[instance_reducible]

instance QuaternionAlgebra.instRing {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] : Ring (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuaternionAlgebra.coe_mul {R : Type u_3} {c₁ c₂ c₃ : R} (x y : R) [CommRing R] : ↑(x * y) = ↑x * ↑y

@[simp]

theorem QuaternionAlgebra.coe_ofNat {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] {n : ℕ} [n.AtLeastTwo] : ↑(OfNat.ofNat n) = OfNat.ofNat n

@[instance_reducible]

instance QuaternionAlgebra.instAlgebra {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] [CommSemiring S] [Algebra S R] : Algebra S (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• One or more equations did not get rendered due to their size.

theorem QuaternionAlgebra.algebraMap_eq {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] (r : R) : (algebraMap R (QuaternionAlgebra R c₁ c₂ c₃)) r = { re := r, imI := 0, imJ := 0, imK := 0 }

theorem QuaternionAlgebra.algebraMap_injective {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] : Function.Injective ⇑(algebraMap R (QuaternionAlgebra R c₁ c₂ c₃))

instance QuaternionAlgebra.instIsTorsionFree {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] : Module.IsTorsionFree R (QuaternionAlgebra R c₁ c₂ c₃)

def QuaternionAlgebra.reₗ {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] : QuaternionAlgebra R c₁ c₂ c₃ →ₗ[R] R

QuaternionAlgebra.re as a LinearMap

Equations

• QuaternionAlgebra.reₗ c₁ c₂ c₃ = { toFun := QuaternionAlgebra.re, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem QuaternionAlgebra.reₗ_apply {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] (self : QuaternionAlgebra R c₁ c₂ c₃) : (reₗ c₁ c₂ c₃) self = self.re

def QuaternionAlgebra.imIₗ {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] : QuaternionAlgebra R c₁ c₂ c₃ →ₗ[R] R

QuaternionAlgebra.imI as a LinearMap

Equations

• QuaternionAlgebra.imIₗ c₁ c₂ c₃ = { toFun := QuaternionAlgebra.imI, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem QuaternionAlgebra.imIₗ_apply {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] (self : QuaternionAlgebra R c₁ c₂ c₃) : (imIₗ c₁ c₂ c₃) self = self.imI

def QuaternionAlgebra.imJₗ {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] : QuaternionAlgebra R c₁ c₂ c₃ →ₗ[R] R

QuaternionAlgebra.imJ as a LinearMap

Equations

• QuaternionAlgebra.imJₗ c₁ c₂ c₃ = { toFun := QuaternionAlgebra.imJ, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem QuaternionAlgebra.imJₗ_apply {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] (self : QuaternionAlgebra R c₁ c₂ c₃) : (imJₗ c₁ c₂ c₃) self = self.imJ

def QuaternionAlgebra.imKₗ {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] : QuaternionAlgebra R c₁ c₂ c₃ →ₗ[R] R

QuaternionAlgebra.imK as a LinearMap

Equations

• QuaternionAlgebra.imKₗ c₁ c₂ c₃ = { toFun := QuaternionAlgebra.imK, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem QuaternionAlgebra.imKₗ_apply {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] (self : QuaternionAlgebra R c₁ c₂ c₃) : (imKₗ c₁ c₂ c₃) self = self.imK

def QuaternionAlgebra.linearEquivTuple {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] : QuaternionAlgebra R c₁ c₂ c₃ ≃ₗ[R] Fin 4 → R

QuaternionAlgebra.equivTuple as a linear equivalence.

Equations

• QuaternionAlgebra.linearEquivTuple c₁ c₂ c₃ = Equiv.linearEquiv R (QuaternionAlgebra.equivTuple c₁ c₂ c₃)

@[simp]

theorem QuaternionAlgebra.coe_linearEquivTuple {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] : ⇑(linearEquivTuple c₁ c₂ c₃) = ⇑(equivTuple c₁ c₂ c₃)

@[simp]

theorem QuaternionAlgebra.coe_linearEquivTuple_symm {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] : ⇑(linearEquivTuple c₁ c₂ c₃).symm = ⇑(equivTuple c₁ c₂ c₃).symm

noncomputable def QuaternionAlgebra.basisOneIJK {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] : Module.Basis (Fin 4) R (QuaternionAlgebra R c₁ c₂ c₃)

ℍ[R,c₁,c₂,c₃] has a basis over R given by 1, i, j, and k.

Equations

• QuaternionAlgebra.basisOneIJK c₁ c₂ c₃ = Module.Basis.ofEquivFun (QuaternionAlgebra.linearEquivTuple c₁ c₂ c₃)

@[simp]

theorem QuaternionAlgebra.coe_basisOneIJK_repr {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] (q : QuaternionAlgebra R c₁ c₂ c₃) : ⇑((basisOneIJK c₁ c₂ c₃).repr q) = ![q.re, q.imI, q.imJ, q.imK]

instance QuaternionAlgebra.instFinite {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] : Module.Finite R (QuaternionAlgebra R c₁ c₂ c₃)

instance QuaternionAlgebra.instFree {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] : Module.Free R (QuaternionAlgebra R c₁ c₂ c₃)

theorem QuaternionAlgebra.rank_eq_four {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] [StrongRankCondition R] : Module.rank R (QuaternionAlgebra R c₁ c₂ c₃) = 4

theorem QuaternionAlgebra.finrank_eq_four {R : Type u_3} (c₁ c₂ c₃ : R) [CommRing R] [StrongRankCondition R] : Module.finrank R (QuaternionAlgebra R c₁ c₂ c₃) = 4

def QuaternionAlgebra.swapEquiv {R : Type u_3} (c₁ c₃ : R) [CommRing R] : QuaternionAlgebra R c₁ 0 c₃ ≃ₐ[R] QuaternionAlgebra R c₃ 0 c₁

There is a natural equivalence when swapping the first and third coefficients of a quaternion algebra if c₂ is 0.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuaternionAlgebra.imI_swapEquiv_symm_apply {R : Type u_3} (c₁ c₃ : R) [CommRing R] (t : QuaternionAlgebra R c₃ 0 c₁) : ((swapEquiv c₁ c₃).symm t).imI = t.imJ

@[simp]

theorem QuaternionAlgebra.re_swapEquiv_apply {R : Type u_3} (c₁ c₃ : R) [CommRing R] (t : QuaternionAlgebra R c₁ 0 c₃) : ((swapEquiv c₁ c₃) t).re = t.re

@[simp]

theorem QuaternionAlgebra.re_swapEquiv_symm_apply {R : Type u_3} (c₁ c₃ : R) [CommRing R] (t : QuaternionAlgebra R c₃ 0 c₁) : ((swapEquiv c₁ c₃).symm t).re = t.re

@[simp]

theorem QuaternionAlgebra.imJ_swapEquiv_symm_apply {R : Type u_3} (c₁ c₃ : R) [CommRing R] (t : QuaternionAlgebra R c₃ 0 c₁) : ((swapEquiv c₁ c₃).symm t).imJ = t.imI

@[simp]

theorem QuaternionAlgebra.imK_swapEquiv_symm_apply {R : Type u_3} (c₁ c₃ : R) [CommRing R] (t : QuaternionAlgebra R c₃ 0 c₁) : ((swapEquiv c₁ c₃).symm t).imK = -t.imK

@[simp]

theorem QuaternionAlgebra.imI_swapEquiv_apply {R : Type u_3} (c₁ c₃ : R) [CommRing R] (t : QuaternionAlgebra R c₁ 0 c₃) : ((swapEquiv c₁ c₃) t).imI = t.imJ

@[simp]

theorem QuaternionAlgebra.imJ_swapEquiv_apply {R : Type u_3} (c₁ c₃ : R) [CommRing R] (t : QuaternionAlgebra R c₁ 0 c₃) : ((swapEquiv c₁ c₃) t).imJ = t.imI

@[simp]

theorem QuaternionAlgebra.imK_swapEquiv_apply {R : Type u_3} (c₁ c₃ : R) [CommRing R] (t : QuaternionAlgebra R c₁ 0 c₃) : ((swapEquiv c₁ c₃) t).imK = -t.imK

@[simp]

theorem QuaternionAlgebra.coe_sub {R : Type u_3} {c₁ c₂ c₃ : R} (x y : R) [CommRing R] : ↑(x - y) = ↑x - ↑y

@[simp]

theorem QuaternionAlgebra.coe_pow {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [CommRing R] (n : ℕ) : ↑(x ^ n) = ↑x ^ n

theorem QuaternionAlgebra.coe_commutes {R : Type u_3} {c₁ c₂ c₃ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : ↑r * a = a * ↑r

theorem QuaternionAlgebra.coe_commute {R : Type u_3} {c₁ c₂ c₃ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : Commute (↑r) a

theorem QuaternionAlgebra.coe_mul_eq_smul {R : Type u_3} {c₁ c₂ c₃ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : ↑r * a = r • a

theorem QuaternionAlgebra.mul_coe_eq_smul {R : Type u_3} {c₁ c₂ c₃ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : a * ↑r = r • a

@[simp]

theorem QuaternionAlgebra.coe_algebraMap {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] : ⇑(algebraMap R (QuaternionAlgebra R c₁ c₂ c₃)) = coe

theorem QuaternionAlgebra.smul_coe {R : Type u_3} {c₁ c₂ c₃ : R} (x y : R) [CommRing R] : x • ↑y = ↑(x * y)

@[instance_reducible]

instance QuaternionAlgebra.instStarQuaternionAlgebra {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] : Star (QuaternionAlgebra R c₁ c₂ c₃)

Quaternion conjugate.

Equations

• QuaternionAlgebra.instStarQuaternionAlgebra = { star := fun (a : QuaternionAlgebra R c₁ c₂ c₃) => { re := a.re + c₂ * a.imI, imI := -a.imI, imJ := -a.imJ, imK := -a.imK } }

@[simp]

theorem QuaternionAlgebra.re_star {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : (star a).re = a.re + c₂ * a.imI

@[simp]

theorem QuaternionAlgebra.imI_star {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : (star a).imI = -a.imI

@[simp]

theorem QuaternionAlgebra.imJ_star {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : (star a).imJ = -a.imJ

@[simp]

theorem QuaternionAlgebra.imK_star {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : (star a).imK = -a.imK

@[simp]

theorem QuaternionAlgebra.im_star {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : (star a).im = -a.im

@[simp]

theorem QuaternionAlgebra.star_mk {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] (a₁ a₂ a₃ a₄ : R) : star { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } = { re := a₁ + c₂ * a₂, imI := -a₂, imJ := -a₃, imK := -a₄ }

@[instance_reducible]

instance QuaternionAlgebra.instStarRing {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] : StarRing (QuaternionAlgebra R c₁ c₂ c₃)

Equations

• QuaternionAlgebra.instStarRing = { toStar := QuaternionAlgebra.instStarQuaternionAlgebra, star_involutive := ⋯, star_mul := ⋯, star_add := ⋯ }

theorem QuaternionAlgebra.self_add_star' {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : a + star a = ↑(2 * a.re + c₂ * a.imI)

theorem QuaternionAlgebra.self_add_star {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : a + star a = 2 * ↑a.re + ↑c₂ * ↑a.imI

theorem QuaternionAlgebra.star_add_self' {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : star a + a = ↑(2 * a.re + c₂ * a.imI)

theorem QuaternionAlgebra.star_add_self {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : star a + a = 2 * ↑a.re + ↑c₂ * ↑a.imI

theorem QuaternionAlgebra.star_eq_two_re_sub {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : star a = ↑(2 * a.re + c₂ * a.imI) - a

theorem QuaternionAlgebra.comm {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] (r : R) (x : QuaternionAlgebra R c₁ c₂ c₃) : ↑r * x = x * ↑r

instance QuaternionAlgebra.instIsStarNormal {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : IsStarNormal a

@[simp]

theorem QuaternionAlgebra.star_coe {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [CommRing R] : star ↑x = ↑x

@[simp]

theorem QuaternionAlgebra.star_im {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : star a.im = -a.im + ↑c₂ * ↑a.imI

@[simp]

theorem QuaternionAlgebra.star_smul {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (s : S) (a : QuaternionAlgebra R c₁ c₂ c₃) : star (s • a) = s • star a

theorem QuaternionAlgebra.star_smul' {S : Type u_1} {R : Type u_3} {c₁ c₃ : R} [CommRing R] [Monoid S] [DistribMulAction S R] (s : S) (a : QuaternionAlgebra R c₁ 0 c₃) : star (s • a) = s • star a

A version of star_smul for the special case when c₂ = 0, without SMulCommClass S R R.

theorem QuaternionAlgebra.eq_re_of_eq_coe {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] {a : QuaternionAlgebra R c₁ c₂ c₃} {x : R} (h : a = ↑x) : a = ↑a.re

theorem QuaternionAlgebra.eq_re_iff_mem_range_coe {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] {a : QuaternionAlgebra R c₁ c₂ c₃} : a = ↑a.re ↔ a ∈ Set.range coe

@[simp]

theorem QuaternionAlgebra.star_eq_self {R : Type u_3} {c₃ : R} [CommRing R] [NoZeroDivisors R] [CharZero R] {c₁ c₂ : R} {a : QuaternionAlgebra R c₁ c₂ c₃} : star a = a ↔ a = ↑a.re

theorem QuaternionAlgebra.star_eq_neg {R : Type u_3} {c₃ : R} [CommRing R] [NoZeroDivisors R] [CharZero R] {c₁ : R} {a : QuaternionAlgebra R c₁ 0 c₃} : star a = -a ↔ a.re = 0

theorem QuaternionAlgebra.star_mul_eq_coe {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : star a * a = ↑(star a * a).re

theorem QuaternionAlgebra.mul_star_eq_coe {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [CommRing R] : a * star a = ↑(a * star a).re

def QuaternionAlgebra.starAe {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] : QuaternionAlgebra R c₁ c₂ c₃ ≃ₐ[R] (QuaternionAlgebra R c₁ c₂ c₃)ᵐᵒᵖ

Quaternion conjugate as an AlgEquiv to the opposite ring.

Equations

• QuaternionAlgebra.starAe = { toFun := MulOpposite.op ∘ star, invFun := star ∘ MulOpposite.unop, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem QuaternionAlgebra.coe_starAe {R : Type u_3} {c₁ c₂ c₃ : R} [CommRing R] : ⇑starAe = MulOpposite.op ∘ star

def Quaternion (R : Type u_1) [Zero R] [One R] [Neg R] : Type u_1

Space of quaternions over a type, denoted as ℍ[R]. Implemented as a structure with four fields: re, im_i, im_j, and im_k.

Equations

• Quaternion R = QuaternionAlgebra R (-1) 0 (-1)

def Quaternion.«termℍ[_]» : Lean.ParserDescr

Space of quaternions over a type, denoted as ℍ[R]. Implemented as a structure with four fields: re, im_i, im_j, and im_k.

Equations

• One or more equations did not get rendered due to their size.

def Quaternion.equivProd (R : Type u_1) [Zero R] [One R] [Neg R] : Quaternion R ≃ R × R × R × R

The equivalence between the quaternions over R and R × R × R × R.

Equations

• Quaternion.equivProd R = QuaternionAlgebra.equivProd (-1) 0 (-1)

@[simp]

theorem Quaternion.re_equivProd_symm_apply (R : Type u_1) [Zero R] [One R] [Neg R] (a : R × R × R × R) : ((equivProd R).symm a).re = a.1

@[simp]

theorem Quaternion.imI_equivProd_symm_apply (R : Type u_1) [Zero R] [One R] [Neg R] (a : R × R × R × R) : ((equivProd R).symm a).imI = a.2.1

@[simp]

theorem Quaternion.imK_equivProd_symm_apply (R : Type u_1) [Zero R] [One R] [Neg R] (a : R × R × R × R) : ((equivProd R).symm a).imK = a.2.2.2

@[simp]

theorem Quaternion.imJ_equivProd_symm_apply (R : Type u_1) [Zero R] [One R] [Neg R] (a : R × R × R × R) : ((equivProd R).symm a).imJ = a.2.2.1

@[simp]

theorem Quaternion.equivProd_apply (R : Type u_1) [Zero R] [One R] [Neg R] (a : QuaternionAlgebra R (-1) 0 (-1)) : (equivProd R) a = (a.re, a.imI, a.imJ, a.imK)

def Quaternion.equivTuple (R : Type u_1) [Zero R] [One R] [Neg R] : Quaternion R ≃ (Fin 4 → R)

The equivalence between the quaternions over R and Fin 4 → R.

Equations

• Quaternion.equivTuple R = QuaternionAlgebra.equivTuple (-1) 0 (-1)

@[simp]

theorem Quaternion.equivTuple_symm_apply (R : Type u_1) [Zero R] [One R] [Neg R] (a : Fin 4 → R) : (equivTuple R).symm a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }

@[simp]

theorem Quaternion.equivTuple_apply (R : Type u_1) [Zero R] [One R] [Neg R] (x : Quaternion R) : (equivTuple R) x = ![x.re, x.imI, x.imJ, x.imK]

instance instSubsingletonQuaternion {R : Type u_1} [Zero R] [One R] [Neg R] [Subsingleton R] : Subsingleton (Quaternion R)

instance instNontrivialQuaternion {R : Type u_1} [Zero R] [One R] [Neg R] [Nontrivial R] : Nontrivial (Quaternion R)

def Quaternion.coe {R : Type u_3} [CommRing R] : R → Quaternion R

Coercion R → ℍ[R].

Equations

• Quaternion.coe = QuaternionAlgebra.coe

@[instance_reducible]

instance Quaternion.instCoeTC {R : Type u_3} [CommRing R] : CoeTC R (Quaternion R)

Equations

• Quaternion.instCoeTC = { coe := Quaternion.coe }

@[instance_reducible]

instance Quaternion.instSMul {S : Type u_1} {R : Type u_3} [CommRing R] [SMul S R] : SMul S (Quaternion R)

Equations

• Quaternion.instSMul = { smul := Quaternion.instSMul._aux_1 }

@[instance_reducible]

instance Quaternion.instRing {R : Type u_3} [CommRing R] : Ring (Quaternion R)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Quaternion.instInhabited {R : Type u_3} [CommRing R] : Inhabited (Quaternion R)

Equations

• Quaternion.instInhabited = { default := Quaternion.instInhabited._aux_1 }

instance Quaternion.instIsScalarTower {S : Type u_1} {T : Type u_2} {R : Type u_3} [CommRing R] [SMul S T] [SMul S R] [SMul T R] [IsScalarTower S T R] : IsScalarTower S T (Quaternion R)

instance Quaternion.instSMulCommClass {S : Type u_1} {T : Type u_2} {R : Type u_3} [CommRing R] [SMul S R] [SMul T R] [SMulCommClass S T R] : SMulCommClass S T (Quaternion R)

@[instance_reducible]

instance Quaternion.instMulAction {S : Type u_1} {R : Type u_3} [CommRing R] [Monoid S] [MulAction S R] : MulAction S (Quaternion R)

Equations

• Quaternion.instMulAction = { toSMul := Quaternion.instSMul, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible]

instance Quaternion.instDistribMulAction {S : Type u_1} {R : Type u_3} [CommRing R] [Semiring S] [DistribMulAction S R] : DistribMulAction S (Quaternion R)

Equations

• Quaternion.instDistribMulAction = { toMulAction := Quaternion.instMulAction, smul_zero := ⋯, smul_add := ⋯ }

@[instance_reducible]

instance Quaternion.instModule {S : Type u_1} {R : Type u_3} [CommRing R] [Semiring S] [Module S R] : Module S (Quaternion R)

Equations

• Quaternion.instModule = { toDistribMulAction := Quaternion.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

instance Quaternion.algebra {S : Type u_1} {R : Type u_3} [CommRing R] [CommSemiring S] [Algebra S R] : Algebra S (Quaternion R)

Equations

• Quaternion.algebra = { toSMul := Quaternion.instSMul, algebraMap := Quaternion.algebra._aux_1, commutes' := ⋯, smul_def' := ⋯ }

@[instance_reducible]

instance Quaternion.instStar {R : Type u_3} [CommRing R] : Star (Quaternion R)

Equations

• Quaternion.instStar = { star := Quaternion.instStar._aux_1 }

@[instance_reducible]

instance Quaternion.instStarRing {R : Type u_3} [CommRing R] : StarRing (Quaternion R)

Equations

• Quaternion.instStarRing = { toStar := Quaternion.instStar, star_involutive := ⋯, star_mul := ⋯, star_add := ⋯ }

instance Quaternion.instIsStarNormal {R : Type u_3} [CommRing R] (a : Quaternion R) : IsStarNormal a

theorem Quaternion.ext {R : Type u_3} [CommRing R] (a b : Quaternion R) : a.re = b.re → a.imI = b.imI → a.imJ = b.imJ → a.imK = b.imK → a = b

theorem Quaternion.ext_iff {R : Type u_3} [CommRing R] {a b : Quaternion R} : a = b ↔ a.re = b.re ∧ a.imI = b.imI ∧ a.imJ = b.imJ ∧ a.imK = b.imK

def Quaternion.im {R : Type u_3} [CommRing R] (x : Quaternion R) : Quaternion R

The imaginary part of a quaternion.

Equations

• x.im = QuaternionAlgebra.im x

@[simp]

theorem Quaternion.re_im {R : Type u_3} [CommRing R] (a : Quaternion R) : a.im.re = 0

@[simp]

theorem Quaternion.imI_im {R : Type u_3} [CommRing R] (a : Quaternion R) : a.im.imI = a.imI

@[simp]

theorem Quaternion.imJ_im {R : Type u_3} [CommRing R] (a : Quaternion R) : a.im.imJ = a.imJ

@[simp]

theorem Quaternion.imK_im {R : Type u_3} [CommRing R] (a : Quaternion R) : a.im.imK = a.imK

@[simp]

theorem Quaternion.im_idem {R : Type u_3} [CommRing R] (a : Quaternion R) : a.im.im = a.im

@[simp]

theorem Quaternion.re_add_im {R : Type u_3} [CommRing R] (a : Quaternion R) : ↑a.re + a.im = a

@[simp]

theorem Quaternion.sub_im_self {R : Type u_3} [CommRing R] (a : Quaternion R) : a - a.im = ↑a.re

@[simp]

theorem Quaternion.sub_re_self {R : Type u_3} [CommRing R] (a : Quaternion R) : a - ↑a.re = a.im

@[simp]

theorem Quaternion.re_coe {R : Type u_3} [CommRing R] (x : R) : (↑x).re = x

@[simp]

theorem Quaternion.imI_coe {R : Type u_3} [CommRing R] (x : R) : (↑x).imI = 0

@[simp]

theorem Quaternion.imJ_coe {R : Type u_3} [CommRing R] (x : R) : (↑x).imJ = 0

@[simp]

theorem Quaternion.imK_coe {R : Type u_3} [CommRing R] (x : R) : (↑x).imK = 0

@[simp]

theorem Quaternion.im_coe {R : Type u_3} [CommRing R] (x : R) : (↑x).im = 0

theorem Quaternion.re_zero {R : Type u_3} [CommRing R] : QuaternionAlgebra.re 0 = 0

theorem Quaternion.imI_zero {R : Type u_3} [CommRing R] : QuaternionAlgebra.imI 0 = 0

theorem Quaternion.imJ_zero {R : Type u_3} [CommRing R] : QuaternionAlgebra.imJ 0 = 0

theorem Quaternion.imK_zero {R : Type u_3} [CommRing R] : QuaternionAlgebra.imK 0 = 0

theorem Quaternion.im_zero {R : Type u_3} [CommRing R] : im 0 = 0

@[simp]

theorem Quaternion.coe_zero {R : Type u_3} [CommRing R] : ↑0 = 0

theorem Quaternion.re_one {R : Type u_3} [CommRing R] : QuaternionAlgebra.re 1 = 1

theorem Quaternion.imI_one {R : Type u_3} [CommRing R] : QuaternionAlgebra.imI 1 = 0

theorem Quaternion.imJ_one {R : Type u_3} [CommRing R] : QuaternionAlgebra.imJ 1 = 0

theorem Quaternion.imK_one {R : Type u_3} [CommRing R] : QuaternionAlgebra.imK 1 = 0

theorem Quaternion.im_one {R : Type u_3} [CommRing R] : im 1 = 0

@[simp]

theorem Quaternion.coe_one {R : Type u_3} [CommRing R] : ↑1 = 1

@[simp]

theorem Quaternion.re_add {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a + b).re = a.re + b.re

@[simp]

theorem Quaternion.imI_add {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a + b).imI = a.imI + b.imI

@[simp]

theorem Quaternion.imJ_add {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a + b).imJ = a.imJ + b.imJ

@[simp]

theorem Quaternion.imK_add {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a + b).imK = a.imK + b.imK

@[simp]

theorem Quaternion.im_add {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a + b).im = a.im + b.im

@[simp]

theorem Quaternion.coe_add {R : Type u_3} [CommRing R] (x y : R) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem Quaternion.re_neg {R : Type u_3} [CommRing R] (a : Quaternion R) : (-a).re = -a.re

@[simp]

theorem Quaternion.imI_neg {R : Type u_3} [CommRing R] (a : Quaternion R) : (-a).imI = -a.imI

@[simp]

theorem Quaternion.imJ_neg {R : Type u_3} [CommRing R] (a : Quaternion R) : (-a).imJ = -a.imJ

@[simp]

theorem Quaternion.imK_neg {R : Type u_3} [CommRing R] (a : Quaternion R) : (-a).imK = -a.imK

@[simp]

theorem Quaternion.im_neg {R : Type u_3} [CommRing R] (a : Quaternion R) : (-a).im = -a.im

@[simp]

theorem Quaternion.coe_neg {R : Type u_3} [CommRing R] (x : R) : ↑(-x) = -↑x

@[simp]

theorem Quaternion.re_sub {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a - b).re = a.re - b.re

@[simp]

theorem Quaternion.imI_sub {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a - b).imI = a.imI - b.imI

@[simp]

theorem Quaternion.imJ_sub {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a - b).imJ = a.imJ - b.imJ

@[simp]

theorem Quaternion.imK_sub {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a - b).imK = a.imK - b.imK

@[simp]

theorem Quaternion.im_sub {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a - b).im = a.im - b.im

@[simp]

theorem Quaternion.coe_sub {R : Type u_3} [CommRing R] (x y : R) : ↑(x - y) = ↑x - ↑y

@[simp]

theorem Quaternion.re_mul {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a * b).re = a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK

@[simp]

theorem Quaternion.imI_mul {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a * b).imI = a.re * b.imI + a.imI * b.re + a.imJ * b.imK - a.imK * b.imJ

@[simp]

theorem Quaternion.imJ_mul {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a * b).imJ = a.re * b.imJ - a.imI * b.imK + a.imJ * b.re + a.imK * b.imI

@[simp]

theorem Quaternion.imK_mul {R : Type u_3} [CommRing R] (a b : Quaternion R) : (a * b).imK = a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re

@[simp]

theorem Quaternion.coe_mul {R : Type u_3} [CommRing R] (x y : R) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem Quaternion.coe_pow {R : Type u_3} [CommRing R] (x : R) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

@[simp]

theorem Quaternion.re_natCast {R : Type u_3} [CommRing R] (n : ℕ) : (↑n).re = ↑n

@[simp]

theorem Quaternion.imI_natCast {R : Type u_3} [CommRing R] (n : ℕ) : (↑n).imI = 0

@[simp]

theorem Quaternion.imJ_natCast {R : Type u_3} [CommRing R] (n : ℕ) : (↑n).imJ = 0

@[simp]

theorem Quaternion.imK_natCast {R : Type u_3} [CommRing R] (n : ℕ) : (↑n).imK = 0

@[simp]

theorem Quaternion.im_natCast {R : Type u_3} [CommRing R] (n : ℕ) : (↑n).im = 0

theorem Quaternion.coe_natCast {R : Type u_3} [CommRing R] (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem Quaternion.re_intCast {R : Type u_3} [CommRing R] (z : ℤ) : (↑z).re = ↑z

@[simp]

theorem Quaternion.imI_intCast {R : Type u_3} [CommRing R] (z : ℤ) : (↑z).imI = 0

@[simp]

theorem Quaternion.imJ_intCast {R : Type u_3} [CommRing R] (z : ℤ) : (↑z).imJ = 0

@[simp]

theorem Quaternion.imK_intCast {R : Type u_3} [CommRing R] (z : ℤ) : (↑z).imK = 0

@[simp]

theorem Quaternion.im_intCast {R : Type u_3} [CommRing R] (z : ℤ) : (↑z).im = 0

theorem Quaternion.coe_intCast {R : Type u_3} [CommRing R] (z : ℤ) : ↑↑z = ↑z

theorem Quaternion.coe_injective {R : Type u_3} [CommRing R] : Function.Injective coe

@[simp]

theorem Quaternion.coe_inj {R : Type u_3} [CommRing R] {x y : R} : ↑x = ↑y ↔ x = y

@[simp]

theorem Quaternion.re_smul {S : Type u_1} {R : Type u_3} [CommRing R] (a : Quaternion R) [SMul S R] (s : S) : (s • a).re = s • a.re

@[simp]

theorem Quaternion.imI_smul {S : Type u_1} {R : Type u_3} [CommRing R] (a : Quaternion R) [SMul S R] (s : S) : (s • a).imI = s • a.imI

@[simp]

theorem Quaternion.imJ_smul {S : Type u_1} {R : Type u_3} [CommRing R] (a : Quaternion R) [SMul S R] (s : S) : (s • a).imJ = s • a.imJ

@[simp]

theorem Quaternion.imK_smul {S : Type u_1} {R : Type u_3} [CommRing R] (a : Quaternion R) [SMul S R] (s : S) : (s • a).imK = s • a.imK

@[simp]

theorem Quaternion.im_smul {S : Type u_1} {R : Type u_3} [CommRing R] (a : Quaternion R) [SMulZeroClass S R] (s : S) : (s • a).im = s • a.im

@[simp]

theorem Quaternion.coe_smul {S : Type u_1} {R : Type u_3} [CommRing R] [SMulZeroClass S R] (s : S) (r : R) : ↑(s • r) = s • ↑r

theorem Quaternion.coe_commutes {R : Type u_3} [CommRing R] (r : R) (a : Quaternion R) : ↑r * a = a * ↑r

theorem Quaternion.coe_commute {R : Type u_3} [CommRing R] (r : R) (a : Quaternion R) : Commute (↑r) a

theorem Quaternion.coe_mul_eq_smul {R : Type u_3} [CommRing R] (r : R) (a : Quaternion R) : ↑r * a = r • a

theorem Quaternion.mul_coe_eq_smul {R : Type u_3} [CommRing R] (r : R) (a : Quaternion R) : a * ↑r = r • a

@[simp]

theorem Quaternion.algebraMap_def {R : Type u_3} [CommRing R] : ⇑(algebraMap R (Quaternion R)) = coe

theorem Quaternion.algebraMap_injective {R : Type u_3} [CommRing R] : Function.Injective ⇑(algebraMap R (Quaternion R))

theorem Quaternion.smul_coe {R : Type u_3} [CommRing R] (x y : R) : x • ↑y = ↑(x * y)

instance Quaternion.instFinite {R : Type u_3} [CommRing R] : Module.Finite R (Quaternion R)

instance Quaternion.instFree {R : Type u_3} [CommRing R] : Module.Free R (Quaternion R)

theorem Quaternion.rank_eq_four {R : Type u_3} [CommRing R] [StrongRankCondition R] : Module.rank R (Quaternion R) = 4

theorem Quaternion.finrank_eq_four {R : Type u_3} [CommRing R] [StrongRankCondition R] : Module.finrank R (Quaternion R) = 4

@[simp]

theorem Quaternion.re_star {R : Type u_3} [CommRing R] (a : Quaternion R) : (star a).re = a.re

@[simp]

theorem Quaternion.imI_star {R : Type u_3} [CommRing R] (a : Quaternion R) : (star a).imI = -a.imI

@[simp]

theorem Quaternion.imJ_star {R : Type u_3} [CommRing R] (a : Quaternion R) : (star a).imJ = -a.imJ

@[simp]

theorem Quaternion.imK_star {R : Type u_3} [CommRing R] (a : Quaternion R) : (star a).imK = -a.imK

@[simp]

theorem Quaternion.im_star {R : Type u_3} [CommRing R] (a : Quaternion R) : (star a).im = -a.im

theorem Quaternion.self_add_star' {R : Type u_3} [CommRing R] (a : Quaternion R) : a + star a = ↑(2 * a.re)

theorem Quaternion.self_add_star {R : Type u_3} [CommRing R] (a : Quaternion R) : a + star a = 2 * ↑a.re

theorem Quaternion.star_add_self' {R : Type u_3} [CommRing R] (a : Quaternion R) : star a + a = ↑(2 * a.re)

theorem Quaternion.star_add_self {R : Type u_3} [CommRing R] (a : Quaternion R) : star a + a = 2 * ↑a.re

theorem Quaternion.star_eq_two_re_sub {R : Type u_3} [CommRing R] (a : Quaternion R) : star a = ↑(2 * a.re) - a

@[simp]

theorem Quaternion.star_coe {R : Type u_3} [CommRing R] (x : R) : star ↑x = ↑x

@[simp]

theorem Quaternion.star_im {R : Type u_3} [CommRing R] (a : Quaternion R) : star a.im = -a.im

@[simp]

theorem Quaternion.star_smul {S : Type u_1} {R : Type u_3} [CommRing R] [Monoid S] [DistribMulAction S R] (s : S) (a : Quaternion R) : star (s • a) = s • star a

theorem Quaternion.eq_re_of_eq_coe {R : Type u_3} [CommRing R] {a : Quaternion R} {x : R} (h : a = ↑x) : a = ↑a.re

theorem Quaternion.eq_re_iff_mem_range_coe {R : Type u_3} [CommRing R] {a : Quaternion R} : a = ↑a.re ↔ a ∈ Set.range coe

@[simp]

theorem Quaternion.star_eq_self {R : Type u_3} [CommRing R] [NoZeroDivisors R] [CharZero R] {a : Quaternion R} : star a = a ↔ a = ↑a.re

@[simp]

theorem Quaternion.star_eq_neg {R : Type u_3} [CommRing R] [NoZeroDivisors R] [CharZero R] {a : Quaternion R} : star a = -a ↔ a.re = 0

theorem Quaternion.star_mul_eq_coe {R : Type u_3} [CommRing R] (a : Quaternion R) : star a * a = ↑(star a * a).re

theorem Quaternion.mul_star_eq_coe {R : Type u_3} [CommRing R] (a : Quaternion R) : a * star a = ↑(a * star a).re

def Quaternion.starAe {R : Type u_3} [CommRing R] : Quaternion R ≃ₐ[R] (Quaternion R)ᵐᵒᵖ

Quaternion conjugate as an AlgEquiv to the opposite ring.

Equations

• Quaternion.starAe = QuaternionAlgebra.starAe

@[simp]

theorem Quaternion.coe_starAe {R : Type u_3} [CommRing R] : ⇑starAe = MulOpposite.op ∘ star

def Quaternion.normSq {R : Type u_3} [CommRing R] : Quaternion R →*₀ R

Square of the norm.

Equations

• Quaternion.normSq = { toFun := fun (a : Quaternion R) => (a * star a).re, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem Quaternion.normSq_def {R : Type u_3} [CommRing R] (a : Quaternion R) : normSq a = (a * star a).re

theorem Quaternion.normSq_def' {R : Type u_3} [CommRing R] (a : Quaternion R) : normSq a = a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2

theorem Quaternion.normSq_coe {R : Type u_3} [CommRing R] (x : R) : normSq ↑x = x ^ 2

@[simp]

theorem Quaternion.normSq_star {R : Type u_3} [CommRing R] (a : Quaternion R) : normSq (star a) = normSq a

theorem Quaternion.normSq_natCast {R : Type u_3} [CommRing R] (n : ℕ) : normSq ↑n = ↑n ^ 2

theorem Quaternion.normSq_intCast {R : Type u_3} [CommRing R] (z : ℤ) : normSq ↑z = ↑z ^ 2

@[simp]

theorem Quaternion.normSq_neg {R : Type u_3} [CommRing R] (a : Quaternion R) : normSq (-a) = normSq a

theorem Quaternion.self_mul_star {R : Type u_3} [CommRing R] (a : Quaternion R) : a * star a = ↑(normSq a)

theorem Quaternion.star_mul_self {R : Type u_3} [CommRing R] (a : Quaternion R) : star a * a = ↑(normSq a)

theorem Quaternion.im_sq {R : Type u_3} [CommRing R] (a : Quaternion R) : a.im ^ 2 = -↑(normSq a.im)

theorem Quaternion.coe_normSq_add {R : Type u_3} [CommRing R] (a b : Quaternion R) : ↑(normSq (a + b)) = ↑(normSq a) + a * star b + b * star a + ↑(normSq b)

theorem Quaternion.normSq_smul {R : Type u_3} [CommRing R] (r : R) (q : Quaternion R) : normSq (r • q) = r ^ 2 * normSq q

theorem Quaternion.normSq_add {R : Type u_3} [CommRing R] (a b : Quaternion R) : normSq (a + b) = normSq a + normSq b + 2 * (a * star b).re

@[simp]

theorem Quaternion.normSq_eq_zero {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {a : Quaternion R} : normSq a = 0 ↔ a = 0

theorem Quaternion.normSq_ne_zero {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {a : Quaternion R} : normSq a ≠ 0 ↔ a ≠ 0

@[simp]

theorem Quaternion.normSq_nonneg {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {a : Quaternion R} : 0 ≤ normSq a

@[simp]

theorem Quaternion.normSq_le_zero {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {a : Quaternion R} : normSq a ≤ 0 ↔ a = 0

instance Quaternion.instNontrivial {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] : Nontrivial (Quaternion R)

instance Quaternion.instNoZeroDivisors {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] : NoZeroDivisors (Quaternion R)

instance Quaternion.instIsDomain {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] : IsDomain (Quaternion R)

theorem Quaternion.sq_eq_normSq {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {a : Quaternion R} : a ^ 2 = ↑(normSq a) ↔ a = ↑a.re

theorem Quaternion.sq_eq_neg_normSq {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {a : Quaternion R} : a ^ 2 = -↑(normSq a) ↔ a.re = 0

@[instance_reducible]

instance Quaternion.instNNRatCast {R : Type u_1} [Field R] : NNRatCast (Quaternion R)

Equations

• Quaternion.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => ↑↑q }

@[instance_reducible]

instance Quaternion.instRatCast {R : Type u_1} [Field R] : RatCast (Quaternion R)

Equations

• Quaternion.instRatCast = { ratCast := fun (q : ℚ) => ↑↑q }

@[simp]

theorem Quaternion.re_nnratCast {R : Type u_1} [Field R] (q : ℚ≥0) : (↑q).re = ↑q

@[simp]

theorem Quaternion.im_nnratCast {R : Type u_1} [Field R] (q : ℚ≥0) : (↑q).im = 0

@[simp]

theorem Quaternion.imI_nnratCast {R : Type u_1} [Field R] (q : ℚ≥0) : (↑q).imI = 0

@[simp]

theorem Quaternion.imJ_nnratCast {R : Type u_1} [Field R] (q : ℚ≥0) : (↑q).imJ = 0

@[simp]

theorem Quaternion.imK_nnratCast {R : Type u_1} [Field R] (q : ℚ≥0) : (↑q).imK = 0

@[simp]

theorem Quaternion.re_ratCast {R : Type u_1} [Field R] (q : ℚ) : (↑q).re = ↑q

@[simp]

theorem Quaternion.im_ratCast {R : Type u_1} [Field R] (q : ℚ) : (↑q).im = 0

@[simp]

theorem Quaternion.imI_ratCast {R : Type u_1} [Field R] (q : ℚ) : (↑q).imI = 0

@[simp]

theorem Quaternion.imJ_ratCast {R : Type u_1} [Field R] (q : ℚ) : (↑q).imJ = 0

@[simp]

theorem Quaternion.imK_ratCast {R : Type u_1} [Field R] (q : ℚ) : (↑q).imK = 0

theorem Quaternion.coe_nnratCast {R : Type u_1} [Field R] (q : ℚ≥0) : ↑↑q = ↑q

theorem Quaternion.coe_ratCast {R : Type u_1} [Field R] (q : ℚ) : ↑↑q = ↑q

theorem Quaternion.coe_ofScientific {R : Type u_1} [Field R] (m : ℕ) (s : Bool) (e : ℕ) : ↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e

@[simp]

theorem Quaternion.re_ofScientific {R : Type u_1} [Field R] (m : ℕ) (s : Bool) (e : ℕ) : QuaternionAlgebra.re (OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e

@[simp]

theorem Quaternion.imI_ofScientific {R : Type u_1} [Field R] (m : ℕ) (s : Bool) (e : ℕ) : QuaternionAlgebra.imI (OfScientific.ofScientific m s e) = 0

@[simp]

theorem Quaternion.imJ_ofScientific {R : Type u_1} [Field R] (m : ℕ) (s : Bool) (e : ℕ) : QuaternionAlgebra.imJ (OfScientific.ofScientific m s e) = 0

@[simp]

theorem Quaternion.imK_ofScientific {R : Type u_1} [Field R] (m : ℕ) (s : Bool) (e : ℕ) : QuaternionAlgebra.imK (OfScientific.ofScientific m s e) = 0

@[instance_reducible]

instance Quaternion.instInv {R : Type u_1} [Field R] : Inv (Quaternion R)

Equations

• Quaternion.instInv = { inv := fun (a : Quaternion R) => (Quaternion.normSq a)⁻¹ • star a }

theorem Quaternion.inv_def {R : Type u_1} [Field R] (a : Quaternion R) : a⁻¹ = (normSq a)⁻¹ • star a

@[instance_reducible]

instance Quaternion.instGroupWithZero {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] : GroupWithZero (Quaternion R)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Quaternion.coe_inv {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (x : R) : ↑x⁻¹ = (↑x)⁻¹

@[simp]

theorem Quaternion.coe_div {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (x y : R) : ↑(x / y) = ↑x / ↑y

@[simp]

theorem Quaternion.coe_zpow {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (x : R) (z : ℤ) : ↑(x ^ z) = ↑x ^ z

@[instance_reducible]

instance Quaternion.instDivisionRing {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] : DivisionRing (Quaternion R)

Equations

• One or more equations did not get rendered due to their size.

theorem Quaternion.normSq_inv {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (a : Quaternion R) : normSq a⁻¹ = (normSq a)⁻¹

theorem Quaternion.normSq_div {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (a b : Quaternion R) : normSq (a / b) = normSq a / normSq b

theorem Quaternion.normSq_zpow {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (a : Quaternion R) (z : ℤ) : normSq (a ^ z) = normSq a ^ z

theorem Quaternion.normSq_ratCast {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (q : ℚ) : ↑(normSq ↑q) = ↑q ^ 2

theorem Cardinal.mk_quaternionAlgebra {R : Type u_1} (c₁ c₂ c₃ : R) : mk (QuaternionAlgebra R c₁ c₂ c₃) = mk R ^ 4

The cardinality of a quaternion algebra, as a type.

@[simp]

theorem Cardinal.mk_quaternionAlgebra_of_infinite {R : Type u_1} (c₁ c₂ c₃ : R) [Infinite R] : mk (QuaternionAlgebra R c₁ c₂ c₃) = mk R

theorem Cardinal.mk_univ_quaternionAlgebra {R : Type u_1} (c₁ c₂ c₃ : R) : mk ↑Set.univ = mk R ^ 4

The cardinality of a quaternion algebra, as a set.

theorem Cardinal.mk_univ_quaternionAlgebra_of_infinite {R : Type u_1} (c₁ c₂ c₃ : R) [Infinite R] : mk ↑Set.univ = mk R

@[instance_reducible]

instance Cardinal.instReprQuaternionAlgebra {R : Type u_1} [Repr R] {a b c : R} : Repr (QuaternionAlgebra R a b c)

Show the quaternion ⟨w, x, y, z⟩ as a string "{ re := w, imI := x, imJ := y, imK := z }".

For the typical case of quaternions over ℝ, each component will show as a Cauchy sequence due to the way Real numbers are represented.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Cardinal.mk_quaternion (R : Type u_1) [Zero R] [One R] [Neg R] : mk (Quaternion R) = mk R ^ 4

The cardinality of the quaternions, as a type.

theorem Cardinal.mk_quaternion_of_infinite (R : Type u_1) [Zero R] [One R] [Neg R] [Infinite R] : mk (Quaternion R) = mk R

theorem Cardinal.mk_univ_quaternion (R : Type u_1) [Zero R] [One R] [Neg R] : mk ↑Set.univ = mk R ^ 4

The cardinality of the quaternions, as a set.

theorem Cardinal.mk_univ_quaternion_of_infinite (R : Type u_1) [Zero R] [One R] [Neg R] [Infinite R] : mk ↑Set.univ = mk R