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 {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

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

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

• re : R

  Real part of a quaternion.

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

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.

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.

@[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_imJ {R : Type u_1} (c₁ : R) (c₂ : R) (a : R × R × R × R) : (↑(QuaternionAlgebra.equivProd c₁ c₂).symm a).imJ = a.snd.snd.fst

@[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.snd.snd.snd

@[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.fst

@[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.snd.fst

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.

@[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.

@[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

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[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.instZeroQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : Zero (QuaternionAlgebra R c₁ c₂)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem QuaternionAlgebra.zero_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : 0.imK = 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.instInhabitedQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : Inhabited (QuaternionAlgebra R c₁ c₂)

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem QuaternionAlgebra.one_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : 1.imK = 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.instAddQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : Add (QuaternionAlgebra R c₁ c₂)

@[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₂) : QuaternionAlgebra.im (a + b) = QuaternionAlgebra.im a + QuaternionAlgebra.im b

@[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.instNegQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : Neg (QuaternionAlgebra R c₁ c₂)

@[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₂) : QuaternionAlgebra.im (-a) = -QuaternionAlgebra.im a

@[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.instSubQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : Sub (QuaternionAlgebra R c₁ c₂)

@[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₂) : QuaternionAlgebra.im (a - b) = QuaternionAlgebra.im a - QuaternionAlgebra.im b

@[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) : QuaternionAlgebra.im ↑x = 0

@[simp]

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

@[simp]

theorem QuaternionAlgebra.sub_self_im {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) : a - QuaternionAlgebra.im a = ↑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 = QuaternionAlgebra.im a

instance QuaternionAlgebra.instMulQuaternionAlgebra {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.

@[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.instSMulQuaternionAlgebra {S : Type u_1} {R : Type u_3} {c₁ : R} {c₂ : R} [SMul S R] : SMul S (QuaternionAlgebra R c₁ c₂)

instance QuaternionAlgebra.instIsScalarTowerQuaternionAlgebraInstSMulQuaternionAlgebraInstSMulQuaternionAlgebra {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₂)

instance QuaternionAlgebra.instSMulCommClassQuaternionAlgebraInstSMulQuaternionAlgebraInstSMulQuaternionAlgebra {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₂)

@[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) : QuaternionAlgebra.im (s • a) = s • QuaternionAlgebra.im a

@[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.instAddCommGroupQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} : AddCommGroup (QuaternionAlgebra R c₁ c₂)

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[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.instAlgebraQuaternionAlgebraToSemiringInstRing {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₂)

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 }

@[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

@[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

@[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

@[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

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.

@[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) : ↑(LinearEquiv.symm (QuaternionAlgebra.linearEquivTuple c₁ c₂)) = ↑(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.

@[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.instFiniteQuaternionAlgebraToSemiringToCommSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingToModuleToSemiringInstAlgebraQuaternionAlgebraToSemiringInstRingId {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) : Module.Finite R (QuaternionAlgebra R c₁ c₂)

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

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.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.

@[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₂) : QuaternionAlgebra.im (star a) = -QuaternionAlgebra.im a

@[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₂)

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.instIsStarNormalQuaternionAlgebraInstMulQuaternionAlgebraInstStarQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) : IsStarNormal a

@[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 (QuaternionAlgebra.im a) = -QuaternionAlgebra.im a

@[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.

@[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.

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

@[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.snd.fst

@[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.snd.snd.snd

@[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.fst

@[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.snd.snd.fst

@[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.

@[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.

@[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]

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

Coercion R → ℍ[R].

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

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

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

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

instance Quaternion.instIsScalarTowerQuaternionToOneToSemiringToCommSemiringToNegToRingInstSMulQuaternionToOneToSemiringToCommSemiringToNegToRingInstSMulQuaternionToOneToSemiringToCommSemiringToNegToRing {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.instSMulCommClassQuaternionToOneToSemiringToCommSemiringToNegToRingInstSMulQuaternionToOneToSemiringToCommSemiringToNegToRingInstSMulQuaternionToOneToSemiringToCommSemiringToNegToRing {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 Quaternion.algebra {S : Type u_1} {R : Type u_3} [CommRing R] [CommSemiring S] [Algebra S R] : Algebra S (Quaternion R)

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

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

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

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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) : Quaternion.im ↑x = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Quaternion.zero_imK {R : Type u_3} [CommRing R] : 0.imK = 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] : 1.re = 1

@[simp]

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

@[simp]

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

@[simp]

theorem Quaternion.one_imK {R : Type u_3} [CommRing R] : 1.imK = 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) : Quaternion.im (a + b) = Quaternion.im a + Quaternion.im b

@[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) : Quaternion.im (-a) = -Quaternion.im a

@[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) : Quaternion.im (a - b) = Quaternion.im a - Quaternion.im b

@[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.nat_cast_re {R : Type u_3} [CommRing R] (n : ℕ) : (↑n).re = ↑n

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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) : Quaternion.im (s • a) = s • Quaternion.im a

@[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.smul_coe {R : Type u_3} [CommRing R] (x : R) (y : R) : x • ↑y = ↑(x * y)

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

instance Quaternion.instFreeQuaternionToOneToSemiringToCommSemiringToNegToRingToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingToModuleToSemiringAlgebraId {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] : 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) : Quaternion.im (star a) = -Quaternion.im a

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 (Quaternion.im a) = -Quaternion.im a

@[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.

@[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.

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_nat_cast {R : Type u_3} [CommRing R] (n : ℕ) : ↑Quaternion.normSq ↑n = ↑n ^ 2

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

@[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) : Quaternion.im a ^ 2 = -↑(↑Quaternion.normSq (Quaternion.im a))

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)

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

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

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)

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

@[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.instRatCastQuaternionToOneToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringToLinearOrderedSemifieldToNegToRingToStrictOrderedRingToLinearOrderedRingToLinearOrderedCommRing {R : Type u_1} [LinearOrderedField R] : RatCast (Quaternion R)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

instance Quaternion.instDivisionRingQuaternionToOneToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringToLinearOrderedSemifieldToNegToRingToStrictOrderedRingToLinearOrderedRingToLinearOrderedCommRing {R : Type u_1} [LinearOrderedField R] : DivisionRing (Quaternion R)

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_rat_cast {R : Type u_1} [LinearOrderedField R] (q : ℚ) : ↑(↑Quaternion.normSq ↑q) = ↑q ^ 2

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

@[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