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, ℍ[R, a, b] : quaternion algebra with coefficients a, b
• Quaternion R, ℍ[R] : the space of quaternions, a.k.a. QuaternionAlgebra R (-1) (-1);
• Quaternion.normSq : square of the norm of a quaternion;

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

• Ring ℍ[R, a, b], StarRing ℍ[R, a, b], and Algebra R ℍ[R, a, b] : 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₂] : QuaternionAlgebra R c₁ 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

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

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

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

Quaternion algebra over a type with fixed coefficients $a=i^2$ and $b=j^2$. Implemented as a structure with four fields: re, imI, imJ, and imK.

• re : R

  Real part of a quaternion.

• imI : R
• imJ : R
• imK : R

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

Quaternion algebra over a type with fixed coefficients $a=i^2$ and $b=j^2$. 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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def QuaternionAlgebra.equivProd {R : Type u_1} (c₁ : R) (c₂ : R) : QuaternionAlgebra R 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.equivTuple_symm_apply {R : Type u_1} (c₁ : R) (c₂ : R) (a : Fin 4 → R) : (QuaternionAlgebra.equivTuple c₁ c₂).symm a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }

def QuaternionAlgebra.equivTuple {R : Type u_1} (c₁ : R) (c₂ : R) : QuaternionAlgebra R 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_apply {R : Type u_1} (c₁ : R) (c₂ : R) (x : QuaternionAlgebra R c₁ c₂) : (QuaternionAlgebra.equivTuple c₁ c₂) x = ![x.re, x.imI, x.imJ, x.imK]

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

The imaginary part of a quaternion.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

Equations

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

@[simp]

theorem QuaternionAlgebra.zero_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : Quaternion.re 0 = 0

@[simp]

theorem QuaternionAlgebra.zero_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : Quaternion.imI 0 = 0

@[simp]

theorem QuaternionAlgebra.zero_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : Quaternion.imJ 0 = 0

@[simp]

theorem QuaternionAlgebra.zero_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : Quaternion.imK 0 = 0

@[simp]

theorem QuaternionAlgebra.zero_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : QuaternionAlgebra.im 0 = 0

@[simp]

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

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

Equations

• QuaternionAlgebra.instInhabited = { default := 0 }

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

Equations

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

@[simp]

theorem QuaternionAlgebra.one_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : Quaternion.re 1 = 1

@[simp]

theorem QuaternionAlgebra.one_imI {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : Quaternion.imI 1 = 0

@[simp]

theorem QuaternionAlgebra.one_imJ {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : Quaternion.imJ 1 = 0

@[simp]

theorem QuaternionAlgebra.one_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : Quaternion.imK 1 = 0

@[simp]

theorem QuaternionAlgebra.one_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : QuaternionAlgebra.im 1 = 0

@[simp]

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

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

Equations

• QuaternionAlgebra.instAdd = { add := fun (a b : QuaternionAlgebra R 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.add_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) : (a + b).re = a.re + b.re

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem QuaternionAlgebra.mk_add_mk {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) (b₁ : R) (b₂ : R) (b₃ : R) (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.coe_add {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) (y : R) : ↑(x + y) = ↑x + ↑y

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• QuaternionAlgebra.instSub = { sub := fun (a b : QuaternionAlgebra R 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.sub_re {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) (b : QuaternionAlgebra R c₁ c₂) : (a - b).re = a.re - b.re

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem QuaternionAlgebra.mk_sub_mk {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) (b₁ : R) (b₂ : R) (b₃ : R) (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.coe_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) : (↑x).im = 0

@[simp]

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

@[simp]

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

@[simp]

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

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

Multiplication is given by

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem QuaternionAlgebra.mk_mul_mk {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a₁ : R) (a₂ : R) (a₃ : R) (a₄ : R) (b₁ : R) (b₂ : R) (b₃ : R) (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₄, imI := a₁ * b₂ + a₂ * b₁ - c₂ * a₃ * b₄ + c₂ * a₄ * b₃, imJ := a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ - c₁ * a₄ * b₂, imK := a₁ * b₄ + a₂ * b₃ - a₃ * b₂ + a₄ * b₁ }

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem QuaternionAlgebra.smul_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) {S : Type u_4} [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₁ : R} {c₂ : R} [SMul S R] (s : S) (re : R) (im_i : R) (im_j : R) (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 }

@[simp]

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

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

Equations

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

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

Equations

• QuaternionAlgebra.instAddCommGroupWithOne = AddCommGroupWithOne.mk ⋯ ⋯ ⋯ ⋯

@[simp]

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

@[deprecated QuaternionAlgebra.natCast_re]

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

Alias of QuaternionAlgebra.natCast_re.

@[simp]

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

@[deprecated QuaternionAlgebra.natCast_imI]

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

Alias of QuaternionAlgebra.natCast_imI.

@[simp]

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

@[deprecated QuaternionAlgebra.natCast_imJ]

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

Alias of QuaternionAlgebra.natCast_imJ.

@[simp]

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

@[deprecated QuaternionAlgebra.natCast_imK]

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

Alias of QuaternionAlgebra.natCast_imK.

@[simp]

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

@[deprecated QuaternionAlgebra.natCast_im]

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

Alias of QuaternionAlgebra.natCast_im.

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

@[deprecated QuaternionAlgebra.coe_natCast]

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

Alias of QuaternionAlgebra.coe_natCast.

@[simp]

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

@[deprecated QuaternionAlgebra.intCast_re]

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

Alias of QuaternionAlgebra.intCast_re.

@[simp]

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

@[deprecated QuaternionAlgebra.intCast_imI]

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

Alias of QuaternionAlgebra.intCast_imI.

@[simp]

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

@[deprecated QuaternionAlgebra.intCast_imJ]

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

Alias of QuaternionAlgebra.intCast_imJ.

@[simp]

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

@[deprecated QuaternionAlgebra.intCast_imK]

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

Alias of QuaternionAlgebra.intCast_imK.

@[simp]

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

@[deprecated QuaternionAlgebra.intCast_im]

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

Alias of QuaternionAlgebra.intCast_im.

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

@[deprecated QuaternionAlgebra.coe_intCast]

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

Alias of QuaternionAlgebra.coe_intCast.

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

Equations

• QuaternionAlgebra.instRing = let __spread.0 := inferInstanceAs (AddCommGroupWithOne (QuaternionAlgebra R c₁ c₂)); Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

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

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

Equations

• QuaternionAlgebra.instAlgebra = Algebra.mk { toFun := fun (s : S) => ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

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

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

instance QuaternionAlgebra.instNoZeroSMulDivisorsOfNoZeroDivisors {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} [NoZeroDivisors R] : NoZeroSMulDivisors R (QuaternionAlgebra R c₁ c₂)

Equations

• ⋯ = ⋯

@[simp]

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

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

QuaternionAlgebra.re as a LinearMap

Equations

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

@[simp]

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

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

QuaternionAlgebra.imI as a LinearMap

Equations

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

@[simp]

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

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

QuaternionAlgebra.imJ as a LinearMap

Equations

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

@[simp]

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

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

QuaternionAlgebra.imK as a LinearMap

Equations

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

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

QuaternionAlgebra.equivTuple as a linear equivalence.

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

There is a natural equivalence when swapping the coefficients of a quaternion algebra.

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

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

Quaternion conjugate.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• QuaternionAlgebra.instStarRing = StarRing.mk ⋯

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

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

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

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

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

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

Quaternion conjugate as an AlgEquiv to the opposite ring.

Equations

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

@[simp]

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

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def Quaternion.equivProd (R : Type u_1) [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) (-1)

@[simp]

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

def Quaternion.equivTuple (R : Type u_1) [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) (-1)

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Coercion R → ℍ[R].

Equations

• Quaternion.coe = QuaternionAlgebra.coe

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

Equations

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

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

Equations

• Quaternion.instRing = QuaternionAlgebra.instRing

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

Equations

• Quaternion.instInhabited = inferInstanceAs (Inhabited (QuaternionAlgebra R (-1) (-1)))

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

Equations

• Quaternion.instSMul = inferInstanceAs (SMul S (QuaternionAlgebra R (-1) (-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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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 = inferInstanceAs (Algebra S (QuaternionAlgebra R (-1) (-1)))

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

Equations

• Quaternion.instStar = QuaternionAlgebra.instStarQuaternionAlgebra

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

Equations

• Quaternion.instStarRing = QuaternionAlgebra.instStarRing

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

Equations

• ⋯ = ⋯

theorem Quaternion.ext {R : Type u_3} [CommRing R] (a : Quaternion R) (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 : Quaternion R} {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.im_re {R : Type u_3} [CommRing R] (a : Quaternion R) : a.im.re = 0

@[simp]

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

@[simp]

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

@[simp]

theorem Quaternion.im_imK {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_self_im {R : Type u_3} [CommRing R] (a : Quaternion R) : a - a.im = ↑a.re

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Quaternion.neg_im {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.sub_re {R : Type u_3} [CommRing R] (a : Quaternion R) (b : Quaternion R) : (a - b).re = a.re - b.re

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Quaternion.mul_re {R : Type u_3} [CommRing R] (a : Quaternion R) (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.mul_imI {R : Type u_3} [CommRing R] (a : Quaternion R) (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.mul_imJ {R : Type u_3} [CommRing R] (a : Quaternion R) (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.mul_imK {R : Type u_3} [CommRing R] (a : Quaternion R) (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 : R) (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.natCast_re {R : Type u_3} [CommRing R] (n : ℕ) : (↑n).re = ↑n

@[deprecated Quaternion.natCast_re]

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

Alias of Quaternion.natCast_re.

@[simp]

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

@[deprecated Quaternion.natCast_imI]

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

Alias of Quaternion.natCast_imI.

@[simp]

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

@[deprecated Quaternion.natCast_imJ]

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

Alias of Quaternion.natCast_imJ.

@[simp]

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

@[deprecated Quaternion.natCast_imK]

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

Alias of Quaternion.natCast_imK.

@[simp]

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

@[deprecated Quaternion.natCast_im]

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

Alias of Quaternion.natCast_im.

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

@[deprecated Quaternion.coe_natCast]

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

Alias of Quaternion.coe_natCast.

@[simp]

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

@[deprecated Quaternion.intCast_re]

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

Alias of Quaternion.intCast_re.

@[simp]

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

@[deprecated Quaternion.intCast_imI]

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

Alias of Quaternion.intCast_imI.

@[simp]

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

@[deprecated Quaternion.intCast_imJ]

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

Alias of Quaternion.intCast_imJ.

@[simp]

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

@[deprecated Quaternion.intCast_imK]

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

Alias of Quaternion.intCast_imK.

@[simp]

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

@[deprecated Quaternion.intCast_im]

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

Alias of Quaternion.intCast_im.

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

@[deprecated Quaternion.coe_intCast]

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

Alias of Quaternion.coe_intCast.

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

@[simp]

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

@[simp]

theorem Quaternion.smul_re {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.smul_imI {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.smul_imJ {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.smul_imK {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.smul_im {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)) = Quaternion.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 : R) (y : R) : x • ↑y = ↑(x * y)

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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] : FiniteDimensional.finrank R (Quaternion R) = 4

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Quaternion.star_im {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.im_star {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 Quaternion.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] : ⇑Quaternion.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) : Quaternion.normSq a = (a * star a).re

theorem Quaternion.normSq_def' {R : Type u_3} [CommRing R] (a : Quaternion R) : Quaternion.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) : Quaternion.normSq ↑x = x ^ 2

@[simp]

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

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

@[deprecated Quaternion.normSq_natCast]

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

Alias of Quaternion.normSq_natCast.

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

@[deprecated Quaternion.normSq_intCast]

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

Alias of Quaternion.normSq_intCast.

@[simp]

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

instance Quaternion.instNontrivial {R : Type u_1} [LinearOrderedCommRing R] : Nontrivial (Quaternion R)

Equations

• ⋯ = ⋯

instance Quaternion.instNoZeroDivisors {R : Type u_1} [LinearOrderedCommRing R] : NoZeroDivisors (Quaternion R)

Equations

• ⋯ = ⋯

instance Quaternion.instIsDomain {R : Type u_1} [LinearOrderedCommRing R] : IsDomain (Quaternion R)

Equations

• ⋯ = ⋯

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

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

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

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

Equations

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

instance Quaternion.instGroupWithZero {R : Type u_1} [LinearOrderedField R] : GroupWithZero (Quaternion R)

Equations

• Quaternion.instGroupWithZero = let __src := ⋯; let __src_1 := inferInstance; GroupWithZero.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[deprecated Quaternion.ratCast_imI]

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

Alias of Quaternion.ratCast_imI.

@[deprecated Quaternion.ratCast_imJ]

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

Alias of Quaternion.ratCast_imJ.

@[deprecated Quaternion.ratCast_imK]

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

Alias of Quaternion.ratCast_imK.

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

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

@[deprecated Quaternion.coe_ratCast]

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

Alias of Quaternion.coe_ratCast.

instance Quaternion.instDivisionRing {R : Type u_1} [LinearOrderedField 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} [LinearOrderedField R] (a : Quaternion R) : Quaternion.normSq a⁻¹ = (Quaternion.normSq a)⁻¹

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

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

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

@[deprecated Quaternion.normSq_ratCast]

theorem Quaternion.normSq_rat_cast {R : Type u_1} [LinearOrderedField R] (q : ℚ) : ↑(Quaternion.normSq ↑q) = ↑q ^ 2

Alias of Quaternion.normSq_ratCast.

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

The cardinality of a quaternion algebra, as a type.

@[simp]

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

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

The cardinality of a quaternion algebra, as a set.

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

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

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) [One R] [Neg R] : Cardinal.mk (Quaternion R) = Cardinal.mk R ^ 4

The cardinality of the quaternions, as a type.

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

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

The cardinality of the quaternions, as a set.

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