# 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 : } {y : } :
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 : } {y : } (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
Instances For

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.
Instances For
@[simp]
theorem QuaternionAlgebra.equivProd_symm_apply_re {R : Type u_1} (c₁ : R) (c₂ : R) (a : R × R × R × R) :
(.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) :
(.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₂) :
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) :
(.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) :
(.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.
Instances For
@[simp]
theorem QuaternionAlgebra.equivTuple_symm_apply {R : Type u_1} (c₁ : R) (c₂ : R) (a : Fin 4R) :
.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 4R)

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.
Instances For
@[simp]
theorem QuaternionAlgebra.equivTuple_apply {R : Type u_1} (c₁ : R) (c₂ : R) (x : QuaternionAlgebra R 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} [] :
Equations
• =
instance QuaternionAlgebra.instNontrivial {R : Type u_3} {c₁ : R} {c₂ : R} [] :
Equations
• =
def QuaternionAlgebra.im {R : Type u_3} [] {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 }
Instances For
@[simp]
theorem QuaternionAlgebra.im_re {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
a.im.re = 0
@[simp]
theorem QuaternionAlgebra.im_imI {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
a.im.imI = a.imI
@[simp]
theorem QuaternionAlgebra.im_imJ {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
a.im.imJ = a.imJ
@[simp]
theorem QuaternionAlgebra.im_imK {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
a.im.imK = a.imK
@[simp]
theorem QuaternionAlgebra.im_idem {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
a.im.im = a.im
def QuaternionAlgebra.coe {R : Type u_3} [] {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 }
Instances For
instance QuaternionAlgebra.instCoeTC {R : Type u_3} [] {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} [] {c₁ : R} {c₂ : R} (x : R) :
(↑x).re = x
@[simp]
theorem QuaternionAlgebra.coe_imI {R : Type u_3} [] {c₁ : R} {c₂ : R} (x : R) :
(↑x).imI = 0
@[simp]
theorem QuaternionAlgebra.coe_imJ {R : Type u_3} [] {c₁ : R} {c₂ : R} (x : R) :
(↑x).imJ = 0
@[simp]
theorem QuaternionAlgebra.coe_imK {R : Type u_3} [] {c₁ : R} {c₂ : R} (x : R) :
(↑x).imK = 0
theorem QuaternionAlgebra.coe_injective {R : Type u_3} [] {c₁ : R} {c₂ : R} :
Function.Injective QuaternionAlgebra.coe
@[simp]
theorem QuaternionAlgebra.coe_inj {R : Type u_3} [] {c₁ : R} {c₂ : R} {x : R} {y : R} :
x = y x = y
instance QuaternionAlgebra.instZero {R : Type u_3} [] {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} [] {c₁ : R} {c₂ : R} :
@[simp]
theorem QuaternionAlgebra.zero_imI {R : Type u_3} [] {c₁ : R} {c₂ : R} :
@[simp]
theorem QuaternionAlgebra.zero_imJ {R : Type u_3} [] {c₁ : R} {c₂ : R} :
@[simp]
theorem QuaternionAlgebra.zero_imK {R : Type u_3} [] {c₁ : R} {c₂ : R} :
@[simp]
theorem QuaternionAlgebra.zero_im {R : Type u_3} [] {c₁ : R} {c₂ : R} :
@[simp]
theorem QuaternionAlgebra.coe_zero {R : Type u_3} [] {c₁ : R} {c₂ : R} :
0 = 0
instance QuaternionAlgebra.instInhabited {R : Type u_3} [] {c₁ : R} {c₂ : R} :
Equations
• QuaternionAlgebra.instInhabited = { default := 0 }
instance QuaternionAlgebra.instOne {R : Type u_3} [] {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} [] {c₁ : R} {c₂ : R} :
@[simp]
theorem QuaternionAlgebra.one_imI {R : Type u_3} [] {c₁ : R} {c₂ : R} :
@[simp]
theorem QuaternionAlgebra.one_imJ {R : Type u_3} [] {c₁ : R} {c₂ : R} :
@[simp]
theorem QuaternionAlgebra.one_imK {R : Type u_3} [] {c₁ : R} {c₂ : R} :
@[simp]
theorem QuaternionAlgebra.one_im {R : Type u_3} [] {c₁ : R} {c₂ : R} :
@[simp]
theorem QuaternionAlgebra.coe_one {R : Type u_3} [] {c₁ : R} {c₂ : R} :
1 = 1
instance QuaternionAlgebra.instAdd {R : Type u_3} [] {c₁ : R} {c₂ : R} :
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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {c₁ : R} {c₂ : R} (x : R) (y : R) :
(x + y) = x + y
instance QuaternionAlgebra.instNeg {R : Type u_3} [] {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} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
(-a).re = -a.re
@[simp]
theorem QuaternionAlgebra.neg_imI {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
(-a).imI = -a.imI
@[simp]
theorem QuaternionAlgebra.neg_imJ {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
(-a).imJ = -a.imJ
@[simp]
theorem QuaternionAlgebra.neg_imK {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
(-a).imK = -a.imK
@[simp]
theorem QuaternionAlgebra.neg_im {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
(-a).im = -a.im
@[simp]
theorem QuaternionAlgebra.neg_mk {R : Type u_3} [] {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} [] {c₁ : R} {c₂ : R} (x : R) :
(-x) = -x
instance QuaternionAlgebra.instSub {R : Type u_3} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {c₁ : R} {c₂ : R} (x : R) :
(↑x).im = 0
@[simp]
theorem QuaternionAlgebra.re_add_im {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
a.re + a.im = a
@[simp]
theorem QuaternionAlgebra.sub_self_im {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
a - a.im = a.re
@[simp]
theorem QuaternionAlgebra.sub_self_re {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
a - a.re = a.im
instance QuaternionAlgebra.instMul {R : Type u_3} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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] [] :
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] [] :
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} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) {S : Type u_4} [] (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} [] {c₁ : R} {c₂ : R} [] (s : S) (r : R) :
(s r) = s r
instance QuaternionAlgebra.instAddCommGroup {R : Type u_3} [] {c₁ : R} {c₂ : R} :
Equations
instance QuaternionAlgebra.instAddCommGroupWithOne {R : Type u_3} [] {c₁ : R} {c₂ : R} :
Equations
@[simp]
theorem QuaternionAlgebra.natCast_re {R : Type u_3} [] {c₁ : R} {c₂ : R} (n : ) :
(↑n).re = n
@[deprecated QuaternionAlgebra.natCast_re]
theorem QuaternionAlgebra.nat_cast_re {R : Type u_3} [] {c₁ : R} {c₂ : R} (n : ) :
(↑n).re = n

Alias of QuaternionAlgebra.natCast_re.

@[simp]
theorem QuaternionAlgebra.natCast_imI {R : Type u_3} [] {c₁ : R} {c₂ : R} (n : ) :
(↑n).imI = 0
@[deprecated QuaternionAlgebra.natCast_imI]
theorem QuaternionAlgebra.nat_cast_imI {R : Type u_3} [] {c₁ : R} {c₂ : R} (n : ) :
(↑n).imI = 0

Alias of QuaternionAlgebra.natCast_imI.

@[simp]
theorem QuaternionAlgebra.natCast_imJ {R : Type u_3} [] {c₁ : R} {c₂ : R} (n : ) :
(↑n).imJ = 0
@[deprecated QuaternionAlgebra.natCast_imJ]
theorem QuaternionAlgebra.nat_cast_imJ {R : Type u_3} [] {c₁ : R} {c₂ : R} (n : ) :
(↑n).imJ = 0

Alias of QuaternionAlgebra.natCast_imJ.

@[simp]
theorem QuaternionAlgebra.natCast_imK {R : Type u_3} [] {c₁ : R} {c₂ : R} (n : ) :
(↑n).imK = 0
@[deprecated QuaternionAlgebra.natCast_imK]
theorem QuaternionAlgebra.nat_cast_imK {R : Type u_3} [] {c₁ : R} {c₂ : R} (n : ) :
(↑n).imK = 0

Alias of QuaternionAlgebra.natCast_imK.

@[simp]
theorem QuaternionAlgebra.natCast_im {R : Type u_3} [] {c₁ : R} {c₂ : R} (n : ) :
(↑n).im = 0
@[deprecated QuaternionAlgebra.natCast_im]
theorem QuaternionAlgebra.nat_cast_im {R : Type u_3} [] {c₁ : R} {c₂ : R} (n : ) :
(↑n).im = 0

Alias of QuaternionAlgebra.natCast_im.

theorem QuaternionAlgebra.coe_natCast {R : Type u_3} [] {c₁ : R} {c₂ : R} (n : ) :
n = n
@[deprecated QuaternionAlgebra.coe_natCast]
theorem QuaternionAlgebra.coe_nat_cast {R : Type u_3} [] {c₁ : R} {c₂ : R} (n : ) :
n = n

Alias of QuaternionAlgebra.coe_natCast.

@[simp]
theorem QuaternionAlgebra.intCast_re {R : Type u_3} [] {c₁ : R} {c₂ : R} (z : ) :
(↑z).re = z
@[deprecated QuaternionAlgebra.intCast_re]
theorem QuaternionAlgebra.int_cast_re {R : Type u_3} [] {c₁ : R} {c₂ : R} (z : ) :
(↑z).re = z

Alias of QuaternionAlgebra.intCast_re.

@[simp]
theorem QuaternionAlgebra.intCast_imI {R : Type u_3} [] {c₁ : R} {c₂ : R} (z : ) :
(↑z).imI = 0
@[deprecated QuaternionAlgebra.intCast_imI]
theorem QuaternionAlgebra.int_cast_imI {R : Type u_3} [] {c₁ : R} {c₂ : R} (z : ) :
(↑z).imI = 0

Alias of QuaternionAlgebra.intCast_imI.

@[simp]
theorem QuaternionAlgebra.intCast_imJ {R : Type u_3} [] {c₁ : R} {c₂ : R} (z : ) :
(↑z).imJ = 0
@[deprecated QuaternionAlgebra.intCast_imJ]
theorem QuaternionAlgebra.int_cast_imJ {R : Type u_3} [] {c₁ : R} {c₂ : R} (z : ) :
(↑z).imJ = 0

Alias of QuaternionAlgebra.intCast_imJ.

@[simp]
theorem QuaternionAlgebra.intCast_imK {R : Type u_3} [] {c₁ : R} {c₂ : R} (z : ) :
(↑z).imK = 0
@[deprecated QuaternionAlgebra.intCast_imK]
theorem QuaternionAlgebra.int_cast_imK {R : Type u_3} [] {c₁ : R} {c₂ : R} (z : ) :
(↑z).imK = 0

Alias of QuaternionAlgebra.intCast_imK.

@[simp]
theorem QuaternionAlgebra.intCast_im {R : Type u_3} [] {c₁ : R} {c₂ : R} (z : ) :
(↑z).im = 0
@[deprecated QuaternionAlgebra.intCast_im]
theorem QuaternionAlgebra.int_cast_im {R : Type u_3} [] {c₁ : R} {c₂ : R} (z : ) :
(↑z).im = 0

Alias of QuaternionAlgebra.intCast_im.

theorem QuaternionAlgebra.coe_intCast {R : Type u_3} [] {c₁ : R} {c₂ : R} (z : ) :
z = z
@[deprecated QuaternionAlgebra.coe_intCast]
theorem QuaternionAlgebra.coe_int_cast {R : Type u_3} [] {c₁ : R} {c₂ : R} (z : ) :
z = z

Alias of QuaternionAlgebra.coe_intCast.

instance QuaternionAlgebra.instRing {R : Type u_3} [] {c₁ : R} {c₂ : R} :
Ring (QuaternionAlgebra R c₁ c₂)
Equations
@[simp]
theorem QuaternionAlgebra.coe_mul {R : Type u_3} [] {c₁ : R} {c₂ : R} (x : R) (y : R) :
(x * y) = x * y
instance QuaternionAlgebra.instAlgebra {S : Type u_1} {R : Type u_3} [] {c₁ : R} {c₂ : R} [] [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} [] {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} [] {c₁ : R} {c₂ : R} :
instance QuaternionAlgebra.instNoZeroSMulDivisorsOfNoZeroDivisors {R : Type u_3} [] {c₁ : R} {c₂ : R} [] :
Equations
• =
@[simp]
theorem QuaternionAlgebra.reₗ_apply {R : Type u_3} [] (c₁ : R) (c₂ : R) (self : QuaternionAlgebra R c₁ c₂) :
(QuaternionAlgebra.reₗ c₁ c₂) self = self.re
def QuaternionAlgebra.reₗ {R : Type u_3} [] (c₁ : R) (c₂ : R) :

QuaternionAlgebra.re as a LinearMap

Equations
• = { toFun := Quaternion.re, map_add' := , map_smul' := }
Instances For
@[simp]
theorem QuaternionAlgebra.imIₗ_apply {R : Type u_3} [] (c₁ : R) (c₂ : R) (self : QuaternionAlgebra R c₁ c₂) :
(QuaternionAlgebra.imIₗ c₁ c₂) self = self.imI
def QuaternionAlgebra.imIₗ {R : Type u_3} [] (c₁ : R) (c₂ : R) :

QuaternionAlgebra.imI as a LinearMap

Equations
• = { toFun := Quaternion.imI, map_add' := , map_smul' := }
Instances For
@[simp]
theorem QuaternionAlgebra.imJₗ_apply {R : Type u_3} [] (c₁ : R) (c₂ : R) (self : QuaternionAlgebra R c₁ c₂) :
(QuaternionAlgebra.imJₗ c₁ c₂) self = self.imJ
def QuaternionAlgebra.imJₗ {R : Type u_3} [] (c₁ : R) (c₂ : R) :

QuaternionAlgebra.imJ as a LinearMap

Equations
• = { toFun := Quaternion.imJ, map_add' := , map_smul' := }
Instances For
@[simp]
theorem QuaternionAlgebra.imKₗ_apply {R : Type u_3} [] (c₁ : R) (c₂ : R) (self : QuaternionAlgebra R c₁ c₂) :
(QuaternionAlgebra.imKₗ c₁ c₂) self = self.imK
def QuaternionAlgebra.imKₗ {R : Type u_3} [] (c₁ : R) (c₂ : R) :

QuaternionAlgebra.imK as a LinearMap

Equations
• = { toFun := Quaternion.imK, map_add' := , map_smul' := }
Instances For
def QuaternionAlgebra.linearEquivTuple {R : Type u_3} [] (c₁ : R) (c₂ : R) :
QuaternionAlgebra R c₁ c₂ ≃ₗ[R] Fin 4R

QuaternionAlgebra.equivTuple as a linear equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem QuaternionAlgebra.coe_linearEquivTuple {R : Type u_3} [] (c₁ : R) (c₂ : R) :
=
@[simp]
theorem QuaternionAlgebra.coe_linearEquivTuple_symm {R : Type u_3} [] (c₁ : R) (c₂ : R) :
.symm = .symm
noncomputable def QuaternionAlgebra.basisOneIJK {R : Type u_3} [] (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
Instances For
@[simp]
theorem QuaternionAlgebra.coe_basisOneIJK_repr {R : Type u_3} [] (c₁ : R) (c₂ : R) (q : QuaternionAlgebra R c₁ c₂) :
(.repr q) = ![q.re, q.imI, q.imJ, q.imK]
instance QuaternionAlgebra.instFinite {R : Type u_3} [] (c₁ : R) (c₂ : R) :
Equations
• =
instance QuaternionAlgebra.instFree {R : Type u_3} [] (c₁ : R) (c₂ : R) :
Equations
• =
theorem QuaternionAlgebra.rank_eq_four {R : Type u_3} [] (c₁ : R) (c₂ : R) :
Module.rank R (QuaternionAlgebra R c₁ c₂) = 4
theorem QuaternionAlgebra.finrank_eq_four {R : Type u_3} [] (c₁ : R) (c₂ : R) :
@[simp]
theorem QuaternionAlgebra.swapEquiv_apply_imI {R : Type u_3} [] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₁ c₂) :
( t).imI = t.imJ
@[simp]
theorem QuaternionAlgebra.swapEquiv_apply_imK {R : Type u_3} [] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₁ c₂) :
( t).imK = -t.imK
@[simp]
theorem QuaternionAlgebra.swapEquiv_symm_apply_re {R : Type u_3} [] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₂ c₁) :
(.symm t).re = t.re
@[simp]
theorem QuaternionAlgebra.swapEquiv_apply_imJ {R : Type u_3} [] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₁ c₂) :
( t).imJ = t.imI
@[simp]
theorem QuaternionAlgebra.swapEquiv_symm_apply_imK {R : Type u_3} [] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₂ c₁) :
(.symm t).imK = -t.imK
@[simp]
theorem QuaternionAlgebra.swapEquiv_symm_apply_imJ {R : Type u_3} [] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₂ c₁) :
(.symm t).imJ = t.imI
@[simp]
theorem QuaternionAlgebra.swapEquiv_symm_apply_imI {R : Type u_3} [] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₂ c₁) :
(.symm t).imI = t.imJ
@[simp]
theorem QuaternionAlgebra.swapEquiv_apply_re {R : Type u_3} [] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₁ c₂) :
( t).re = t.re
def QuaternionAlgebra.swapEquiv {R : Type u_3} [] (c₁ : R) (c₂ : R) :

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.
Instances For
@[simp]
theorem QuaternionAlgebra.coe_sub {R : Type u_3} [] {c₁ : R} {c₂ : R} (x : R) (y : R) :
(x - y) = x - y
@[simp]
theorem QuaternionAlgebra.coe_pow {R : Type u_3} [] {c₁ : R} {c₂ : R} (x : R) (n : ) :
(x ^ n) = x ^ n
theorem QuaternionAlgebra.coe_commutes {R : Type u_3} [] {c₁ : R} {c₂ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂) :
r * a = a * r
theorem QuaternionAlgebra.coe_commute {R : Type u_3} [] {c₁ : R} {c₂ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂) :
Commute (↑r) a
theorem QuaternionAlgebra.coe_mul_eq_smul {R : Type u_3} [] {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} [] {c₁ : R} {c₂ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂) :
a * r = r a
@[simp]
theorem QuaternionAlgebra.coe_algebraMap {R : Type u_3} [] {c₁ : R} {c₂ : R} :
(algebraMap R (QuaternionAlgebra R c₁ c₂)) = QuaternionAlgebra.coe
theorem QuaternionAlgebra.smul_coe {R : Type u_3} [] {c₁ : R} {c₂ : R} (x : R) (y : R) :
x y = (x * y)
instance QuaternionAlgebra.instStarQuaternionAlgebra {R : Type u_3} [] {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} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
(star a).re = a.re
@[simp]
theorem QuaternionAlgebra.imI_star {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
(star a).imI = -a.imI
@[simp]
theorem QuaternionAlgebra.imJ_star {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
(star a).imJ = -a.imJ
@[simp]
theorem QuaternionAlgebra.imK_star {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
(star a).imK = -a.imK
@[simp]
theorem QuaternionAlgebra.im_star {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
(star a).im = -a.im
@[simp]
theorem QuaternionAlgebra.star_mk {R : Type u_3} [] {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} [] {c₁ : R} {c₂ : R} :
Equations
• QuaternionAlgebra.instStarRing =
theorem QuaternionAlgebra.self_add_star' {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
a + star a = (2 * a.re)
theorem QuaternionAlgebra.self_add_star {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
a + star a = 2 * a.re
theorem QuaternionAlgebra.star_add_self' {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
star a + a = (2 * a.re)
theorem QuaternionAlgebra.star_add_self {R : Type u_3} [] {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} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
star a = (2 * a.re) - a
instance QuaternionAlgebra.instIsStarNormal {R : Type u_3} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
Equations
• =
@[simp]
theorem QuaternionAlgebra.star_coe {R : Type u_3} [] {c₁ : R} {c₂ : R} (x : R) :
star x = x
@[simp]
theorem QuaternionAlgebra.star_im {R : Type u_3} [] {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} [] {c₁ : R} {c₂ : 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} [] {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} [] {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} [] [] [] {c₁ : R} {c₂ : R} {a : QuaternionAlgebra R c₁ c₂} :
star a = a a = a.re
theorem QuaternionAlgebra.star_eq_neg {R : Type u_3} [] [] [] {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} [] {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} [] {c₁ : R} {c₂ : R} (a : QuaternionAlgebra R c₁ c₂) :
a * star a = (a * star a).re
def QuaternionAlgebra.starAe {R : Type u_3} [] {c₁ : R} {c₂ : R} :

Quaternion conjugate as an AlgEquiv to the opposite ring.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem QuaternionAlgebra.coe_starAe {R : Type u_3} [] {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
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Quaternion.equivProd_symm_apply_re (R : Type u_1) [One R] [Neg R] (a : R × R × R × 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) :
(.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) :
(.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) :
(.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)) :
a = (a.re, a.imI, a.imJ, a.imK)
def Quaternion.equivProd (R : Type u_1) [One R] [Neg R] :
R × R × R × R

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

Equations
Instances For
@[simp]
theorem Quaternion.equivTuple_symm_apply (R : Type u_1) [One R] [Neg R] (a : Fin 4R) :
.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] :
(Fin 4R)

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

Equations
Instances For
@[simp]
theorem Quaternion.equivTuple_apply (R : Type u_1) [One R] [Neg R] (x : ) :
= ![x.re, x.imI, x.imJ, x.imK]
instance instSubsingletonQuaternion {R : Type u_1} [One R] [Neg R] [] :
Equations
• =
instance instNontrivialQuaternion {R : Type u_1} [One R] [Neg R] [] :
Equations
• =
def Quaternion.coe {R : Type u_3} [] :
R

Coercion R → ℍ[R].

Equations
• Quaternion.coe = QuaternionAlgebra.coe
Instances For
instance Quaternion.instCoeTC {R : Type u_3} [] :
Equations
• Quaternion.instCoeTC = { coe := Quaternion.coe }
instance Quaternion.instRing {R : Type u_3} [] :
Equations
• Quaternion.instRing = QuaternionAlgebra.instRing
instance Quaternion.instInhabited {R : Type u_3} [] :
Equations
instance Quaternion.instSMul {S : Type u_1} {R : Type u_3} [] [SMul S R] :
Equations
instance Quaternion.instIsScalarTower {S : Type u_1} {T : Type u_2} {R : Type u_3} [] [SMul S T] [SMul S R] [SMul T R] [] :
Equations
• =
instance Quaternion.instSMulCommClass {S : Type u_1} {T : Type u_2} {R : Type u_3} [] [SMul S R] [SMul T R] [] :
Equations
• =
instance Quaternion.algebra {S : Type u_1} {R : Type u_3} [] [] [Algebra S R] :
Equations
instance Quaternion.instStar {R : Type u_3} [] :
Equations
• Quaternion.instStar = QuaternionAlgebra.instStarQuaternionAlgebra
instance Quaternion.instStarRing {R : Type u_3} [] :
Equations
• Quaternion.instStarRing = QuaternionAlgebra.instStarRing
instance Quaternion.instIsStarNormal {R : Type u_3} [] (a : ) :
Equations
• =
theorem Quaternion.ext_iff {R : Type u_3} [] {a : } {b : } :
a = b a.re = b.re a.imI = b.imI a.imJ = b.imJ a.imK = b.imK
theorem Quaternion.ext {R : Type u_3} [] (a : ) (b : ) :
a.re = b.rea.imI = b.imIa.imJ = b.imJa.imK = b.imKa = b
def Quaternion.im {R : Type u_3} [] (x : ) :

The imaginary part of a quaternion.

Equations
• x.im =
Instances For
@[simp]
theorem Quaternion.im_re {R : Type u_3} [] (a : ) :
a.im.re = 0
@[simp]
theorem Quaternion.im_imI {R : Type u_3} [] (a : ) :
a.im.imI = a.imI
@[simp]
theorem Quaternion.im_imJ {R : Type u_3} [] (a : ) :
a.im.imJ = a.imJ
@[simp]
theorem Quaternion.im_imK {R : Type u_3} [] (a : ) :
a.im.imK = a.imK
@[simp]
theorem Quaternion.im_idem {R : Type u_3} [] (a : ) :
a.im.im = a.im
@[simp]
theorem Quaternion.re_add_im {R : Type u_3} [] (a : ) :
a.re + a.im = a
@[simp]
theorem Quaternion.sub_self_im {R : Type u_3} [] (a : ) :
a - a.im = a.re
@[simp]
theorem Quaternion.sub_self_re {R : Type u_3} [] (a : ) :
a - a.re = a.im
@[simp]
theorem Quaternion.coe_re {R : Type u_3} [] (x : R) :
(↑x).re = x
@[simp]
theorem Quaternion.coe_imI {R : Type u_3} [] (x : R) :
(↑x).imI = 0
@[simp]
theorem Quaternion.coe_imJ {R : Type u_3} [] (x : R) :
(↑x).imJ = 0
@[simp]
theorem Quaternion.coe_imK {R : Type u_3} [] (x : R) :
(↑x).imK = 0
@[simp]
theorem Quaternion.coe_im {R : Type u_3} [] (x : R) :
(↑x).im = 0
@[simp]
theorem Quaternion.zero_re {R : Type u_3} [] :
@[simp]
theorem Quaternion.zero_imI {R : Type u_3} [] :
@[simp]
theorem Quaternion.zero_imJ {R : Type u_3} [] :
@[simp]
theorem Quaternion.zero_imK {R : Type u_3} [] :
@[simp]
theorem Quaternion.zero_im {R : Type u_3} [] :
@[simp]
theorem Quaternion.coe_zero {R : Type u_3} [] :
0 = 0
@[simp]
theorem Quaternion.one_re {R : Type u_3} [] :
@[simp]
theorem Quaternion.one_imI {R : Type u_3} [] :
@[simp]
theorem Quaternion.one_imJ {R : Type u_3} [] :
@[simp]
theorem Quaternion.one_imK {R : Type u_3} [] :
@[simp]
theorem Quaternion.one_im {R : Type u_3} [] :
@[simp]
theorem Quaternion.coe_one {R : Type u_3} [] :
1 = 1
@[simp]
theorem Quaternion.add_re {R : Type u_3} [] (a : ) (b : ) :
(a + b).re = a.re + b.re
@[simp]
theorem Quaternion.add_imI {R : Type u_3} [] (a : ) (b : ) :
(a + b).imI = a.imI + b.imI
@[simp]
theorem Quaternion.add_imJ {R : Type u_3} [] (a : ) (b : ) :
(a + b).imJ = a.imJ + b.imJ
@[simp]
theorem Quaternion.add_imK {R : Type u_3} [] (a : ) (b : ) :
(a + b).imK = a.imK + b.imK
@[simp]
theorem Quaternion.add_im {R : Type u_3} [] (a : ) (b : ) :
(a + b).im = a.im + b.im
@[simp]
theorem Quaternion.coe_add {R : Type u_3} [] (x : R) (y : R) :
(x + y) = x + y
@[simp]
theorem Quaternion.neg_re {R : Type u_3} [] (a : ) :
(-a).re = -a.re
@[simp]
theorem Quaternion.neg_imI {R : Type u_3} [] (a : ) :
(-a).imI = -a.imI
@[simp]
theorem Quaternion.neg_imJ {R : Type u_3} [] (a : ) :
(-a).imJ = -a.imJ
@[simp]
theorem Quaternion.neg_imK {R : Type u_3} [] (a : ) :
(-a).imK = -a.imK
@[simp]
theorem Quaternion.neg_im {R : Type u_3} [] (a : ) :
(-a).im = -a.im
@[simp]
theorem Quaternion.coe_neg {R : Type u_3} [] (x : R) :
(-x) = -x
@[simp]
theorem Quaternion.sub_re {R : Type u_3} [] (a : ) (b : ) :
(a - b).re = a.re - b.re
@[simp]
theorem Quaternion.sub_imI {R : Type u_3} [] (a : ) (b : ) :
(a - b).imI = a.imI - b.imI
@[simp]
theorem Quaternion.sub_imJ {R : Type u_3} [] (a : ) (b : ) :
(a - b).imJ = a.imJ - b.imJ
@[simp]
theorem Quaternion.sub_imK {R : Type u_3} [] (a : ) (b : ) :
(a - b).imK = a.imK - b.imK
@[simp]
theorem Quaternion.sub_im {R : Type u_3} [] (a : ) (b : ) :
(a - b).im = a.im - b.im
@[simp]
theorem Quaternion.coe_sub {R : Type u_3} [] (x : R) (y : R) :
(x - y) = x - y
@[simp]
theorem Quaternion.mul_re {R : Type u_3} [] (a : ) (b : ) :
(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} [] (a : ) (b : ) :
(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} [] (a : ) (b : ) :
(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} [] (a : ) (b : ) :
(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} [] (x : R) (y : R) :
(x * y) = x * y
@[simp]
theorem Quaternion.coe_pow {R : Type u_3} [] (x : R) (n : ) :
(x ^ n) = x ^ n
@[simp]
theorem Quaternion.natCast_re {R : Type u_3} [] (n : ) :
(↑n).re = n
@[deprecated Quaternion.natCast_re]
theorem Quaternion.nat_cast_re {R : Type u_3} [] (n : ) :
(↑n).re = n

Alias of Quaternion.natCast_re.

@[simp]
theorem Quaternion.natCast_imI {R : Type u_3} [] (n : ) :
(↑n).imI = 0
@[deprecated Quaternion.natCast_imI]
theorem Quaternion.nat_cast_imI {R : Type u_3} [] (n : ) :
(↑n).imI = 0

Alias of Quaternion.natCast_imI.

@[simp]
theorem Quaternion.natCast_imJ {R : Type u_3} [] (n : ) :
(↑n).imJ = 0
@[deprecated Quaternion.natCast_imJ]
theorem Quaternion.nat_cast_imJ {R : Type u_3} [] (n : ) :
(↑n).imJ = 0

Alias of Quaternion.natCast_imJ.

@[simp]
theorem Quaternion.natCast_imK {R : Type u_3} [] (n : ) :
(↑n).imK = 0
@[deprecated Quaternion.natCast_imK]
theorem Quaternion.nat_cast_imK {R : Type u_3} [] (n : ) :
(↑n).imK = 0

Alias of Quaternion.natCast_imK.

@[simp]
theorem Quaternion.natCast_im {R : Type u_3} [] (n : ) :
(↑n).im = 0
@[deprecated Quaternion.natCast_im]
theorem Quaternion.nat_cast_im {R : Type u_3} [] (n : ) :
(↑n).im = 0

Alias of Quaternion.natCast_im.

theorem Quaternion.coe_natCast {R : Type u_3} [] (n : ) :
n = n
@[deprecated Quaternion.coe_natCast]
theorem Quaternion.coe_nat_cast {R : Type u_3} [] (n : ) :
n = n

Alias of Quaternion.coe_natCast.

@[simp]
theorem Quaternion.intCast_re {R : Type u_3} [] (z : ) :
(↑z).re = z
@[deprecated Quaternion.intCast_re]
theorem Quaternion.int_cast_re {R : Type u_3} [] (z : ) :
(↑z).re = z

Alias of Quaternion.intCast_re.

@[simp]
theorem Quaternion.intCast_imI {R : Type u_3} [] (z : ) :
(↑z).imI = 0
@[deprecated Quaternion.intCast_imI]
theorem Quaternion.int_cast_imI {R : Type u_3} [] (z : ) :
(↑z).imI = 0

Alias of Quaternion.intCast_imI.

@[simp]
theorem Quaternion.intCast_imJ {R : Type u_3} [] (z : ) :
(↑z).imJ = 0
@[deprecated Quaternion.intCast_imJ]
theorem Quaternion.int_cast_imJ {R : Type u_3} [] (z : ) :
(↑z).imJ = 0

Alias of Quaternion.intCast_imJ.

@[simp]
theorem Quaternion.intCast_imK {R : Type u_3} [] (z : ) :
(↑z).imK = 0
@[deprecated Quaternion.intCast_imK]
theorem Quaternion.int_cast_imK {R : Type u_3} [] (z : ) :
(↑z).imK = 0

Alias of Quaternion.intCast_imK.

@[simp]
theorem Quaternion.intCast_im {R : Type u_3} [] (z : ) :
(↑z).im = 0
@[deprecated Quaternion.intCast_im]
theorem Quaternion.int_cast_im {R : Type u_3} [] (z : ) :
(↑z).im = 0

Alias of Quaternion.intCast_im.

theorem Quaternion.coe_intCast {R : Type u_3} [] (z : ) :
z = z
@[deprecated Quaternion.coe_intCast]
theorem Quaternion.coe_int_cast {R : Type u_3} [] (z : ) :
z = z

Alias of Quaternion.coe_intCast.

theorem Quaternion.coe_injective {R : Type u_3} [] :
Function.Injective Quaternion.coe
@[simp]
theorem Quaternion.coe_inj {R : Type u_3} [] {x : R} {y : R} :
x = y x = y
@[simp]
theorem Quaternion.smul_re {S : Type u_1} {R : Type u_3} [] (a : ) [SMul S R] (s : S) :
(s a).re = s a.re
@[simp]
theorem Quaternion.smul_imI {S : Type u_1} {R : Type u_3} [] (a : ) [SMul S R] (s : S) :
(s a).imI = s a.imI
@[simp]
theorem Quaternion.smul_imJ {S : Type u_1} {R : Type u_3} [] (a : ) [SMul S R] (s : S) :
(s a).imJ = s a.imJ
@[simp]
theorem Quaternion.smul_imK {S : Type u_1} {R : Type u_3} [] (a : ) [SMul S R] (s : S) :
(s a).imK = s a.imK
@[simp]
theorem Quaternion.smul_im {S : Type u_1} {R : Type u_3} [] (a : ) [] (s : S) :
(s a).im = s a.im
@[simp]
theorem Quaternion.coe_smul {S : Type u_1} {R : Type u_3} [] [] (s : S) (r : R) :
(s r) = s r
theorem Quaternion.coe_commutes {R : Type u_3} [] (r : R) (a : ) :
r * a = a * r
theorem Quaternion.coe_commute {R : Type u_3} [] (r : R) (a : ) :
Commute (↑r) a
theorem Quaternion.coe_mul_eq_smul {R : Type u_3} [] (r : R) (a : ) :
r * a = r a
theorem Quaternion.mul_coe_eq_smul {R : Type u_3} [] (r : R) (a : ) :
a * r = r a
@[simp]
theorem Quaternion.algebraMap_def {R : Type u_3} [] :
(algebraMap R (Quaternion R)) = Quaternion.coe
theorem Quaternion.smul_coe {R : Type u_3} [] (x : R) (y : R) :
x y = (x * y)
instance Quaternion.instFinite {R : Type u_3} [] :
Equations
• =
instance Quaternion.instFree {R : Type u_3} [] :
Equations
• =
theorem Quaternion.rank_eq_four {R : Type u_3} [] :
= 4
theorem Quaternion.finrank_eq_four {R : Type u_3} [] :
@[simp]
theorem Quaternion.star_re {R : Type u_3} [] (a : ) :
(star a).re = a.re
@[simp]
theorem Quaternion.star_imI {R : Type u_3} [] (a : ) :
(star a).imI = -a.imI
@[simp]
theorem Quaternion.star_imJ {R : Type u_3} [] (a : ) :
(star a).imJ = -a.imJ
@[simp]
theorem Quaternion.star_imK {R : Type u_3} [] (a : ) :
(star a).imK = -a.imK
@[simp]
theorem Quaternion.star_im {R : Type u_3} [] (a : ) :
(star a).im = -a.im
theorem Quaternion.self_add_star' {R : Type u_3} [] (a : ) :
a + star a = (2 * a.re)
theorem Quaternion.self_add_star {R : Type u_3} [] (a : ) :
a + star a = 2 * a.re
theorem Quaternion.star_add_self' {R : Type u_3} [] (a : ) :
star a + a = (2 * a.re)
theorem Quaternion.star_add_self {R : Type u_3} [] (a : ) :
star a + a = 2 * a.re
theorem Quaternion.star_eq_two_re_sub {R : Type u_3} [] (a : ) :
star a = (2 * a.re) - a
@[simp]
theorem Quaternion.star_coe {R : Type u_3} [] (x : R) :
star x = x
@[simp]
theorem Quaternion.im_star {R : Type u_3} [] (a : ) :
star a.im = -a.im
@[simp]
theorem Quaternion.star_smul {S : Type u_1} {R : Type u_3} [] [] [] (s : S) (a : ) :
star (s a) = s star a
theorem Quaternion.eq_re_of_eq_coe {R : Type u_3} [] {a : } {x : R} (h : a = x) :
a = a.re
theorem Quaternion.eq_re_iff_mem_range_coe {R : Type u_3} [] {a : } :
a = a.re a Set.range Quaternion.coe
@[simp]
theorem Quaternion.star_eq_self {R : Type u_3} [] [] [] {a : } :
star a = a a = a.re
@[simp]
theorem Quaternion.star_eq_neg {R : Type u_3} [] [] [] {a : } :
star a = -a a.re = 0
theorem Quaternion.star_mul_eq_coe {R : Type u_3} [] (a : ) :
star a * a = (star a * a).re
theorem Quaternion.mul_star_eq_coe {R : Type u_3} [] (a : ) :
a * star a = (a * star a).re

Quaternion conjugate as an AlgEquiv to the opposite ring.

Equations
• Quaternion.starAe = QuaternionAlgebra.starAe
Instances For
@[simp]
theorem Quaternion.coe_starAe {R : Type u_3} [] :
Quaternion.starAe = MulOpposite.op star
def Quaternion.normSq {R : Type u_3} [] :

Square of the norm.

Equations
• Quaternion.normSq = { toFun := fun (a : ) => (a * star a).re, map_zero' := , map_one' := , map_mul' := }
Instances For
theorem Quaternion.normSq_def {R : Type u_3} [] (a : ) :
Quaternion.normSq a = (a * star a).re
theorem Quaternion.normSq_def' {R : Type u_3} [] (a : ) :
Quaternion.normSq a = a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2
theorem Quaternion.normSq_coe {R : Type u_3} [] (x : R) :
Quaternion.normSq x = x ^ 2
@[simp]
theorem Quaternion.normSq_star {R : Type u_3} [] (a : ) :
Quaternion.normSq (star a) = Quaternion.normSq a
theorem Quaternion.normSq_natCast {R : Type u_3} [] (n : ) :
Quaternion.normSq n = n ^ 2
@[deprecated Quaternion.normSq_natCast]
theorem Quaternion.normSq_nat_cast {R : Type u_3} [] (n : ) :
Quaternion.normSq n = n ^ 2

Alias of Quaternion.normSq_natCast.

theorem Quaternion.normSq_intCast {R : Type u_3} [] (z : ) :
Quaternion.normSq z = z ^ 2
@[deprecated Quaternion.normSq_intCast]
theorem Quaternion.normSq_int_cast {R : Type u_3} [] (z : ) :
Quaternion.normSq z = z ^ 2

Alias of Quaternion.normSq_intCast.

@[simp]
theorem Quaternion.normSq_neg {R : Type u_3} [] (a : ) :
Quaternion.normSq (-a) = Quaternion.normSq a
theorem Quaternion.self_mul_star {R : Type u_3} [] (a : ) :
a * star a = (Quaternion.normSq a)
theorem Quaternion.star_mul_self {R : Type u_3} [] (a : ) :
star a * a = (Quaternion.normSq a)
theorem Quaternion.im_sq {R : Type u_3} [] (a : ) :
a.im ^ 2 = -(Quaternion.normSq a.im)
theorem Quaternion.coe_normSq_add {R : Type u_3} [] (a : ) (b : ) :
(Quaternion.normSq (a + b)) = (Quaternion.normSq a) + a * star b + b * star a + (Quaternion.normSq b)
theorem Quaternion.normSq_smul {R : Type u_3} [] (r : R) (q : ) :
Quaternion.normSq (r q) = r ^ 2 * Quaternion.normSq q
theorem Quaternion.normSq_add {R : Type u_3} [] (a : ) (b : ) :
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} {a : } :
Quaternion.normSq a = 0 a = 0
theorem Quaternion.normSq_ne_zero {R : Type u_1} {a : } :
Quaternion.normSq a 0 a 0
@[simp]
theorem Quaternion.normSq_nonneg {R : Type u_1} {a : } :
0 Quaternion.normSq a
@[simp]
theorem Quaternion.normSq_le_zero {R : Type u_1} {a : } :
Quaternion.normSq a 0 a = 0
instance Quaternion.instNontrivial {R : Type u_1} :
Equations
• =
instance Quaternion.instNoZeroDivisors {R : Type u_1} :
Equations
• =
instance Quaternion.instIsDomain {R : Type u_1} :
Equations
• =
theorem Quaternion.sq_eq_normSq {R : Type u_1} {a : } :
a ^ 2 = (Quaternion.normSq a) a = a.re
theorem Quaternion.sq_eq_neg_normSq {R : Type u_1} {a : } :
a ^ 2 = -(Quaternion.normSq a) a.re = 0
theorem Quaternion.instInv_inv {R : Type u_1} (a : ) :
a⁻¹ = (Quaternion.normSq a)⁻¹ star a
instance Quaternion.instInv {R : Type u_1} :
Equations
• Quaternion.instInv = { inv := fun (a : ) => (Quaternion.normSq a)⁻¹ star a }
instance Quaternion.instGroupWithZero {R : Type u_1} :
Equations
• Quaternion.instGroupWithZero = let __src := ; let __src_1 := inferInstance; GroupWithZero.mk zpowRec
@[simp]
theorem Quaternion.coe_inv {R : Type u_1} (x : R) :
x⁻¹ = (↑x)⁻¹
@[simp]
theorem Quaternion.coe_div {R : Type u_1} (x : R) (y : R) :
(x / y) = x / y
@[simp]
theorem Quaternion.coe_zpow {R : Type u_1} (x : R) (z : ) :
(x ^ z) = x ^ z
instance Quaternion.instNNRatCast {R : Type u_1} :
Equations
• Quaternion.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => q }
instance Quaternion.instRatCast {R : Type u_1} :
Equations
• Quaternion.instRatCast = { ratCast := fun (q : ) => q }
@[simp]
theorem Quaternion.re_nnratCast {R : Type u_1} (q : ℚ≥0) :
(↑q).re = q
@[simp]
theorem Quaternion.im_nnratCast {R : Type u_1} (q : ℚ≥0) :
(↑q).im = 0
@[simp]
theorem Quaternion.imI_nnratCast {R : Type u_1} (q : ℚ≥0) :
(↑q).imI = 0
@[simp]
theorem Quaternion.imJ_nnratCast {R : Type u_1} (q : ℚ≥0) :
(↑q).imJ = 0
@[simp]
theorem Quaternion.imK_nnratCast {R : Type u_1} (q : ℚ≥0) :
(↑q).imK = 0
@[simp]
theorem Quaternion.ratCast_re {R : Type u_1} (q : ) :
(↑q).re = q
@[simp]
theorem Quaternion.ratCast_im {R : Type u_1} (q : ) :
(↑q).im = 0
@[simp]
theorem Quaternion.ratCast_imI {R : Type u_1} (q : ) :
(↑q).imI = 0
@[simp]
theorem Quaternion.ratCast_imJ {R : Type u_1} (q : ) :
(↑q).imJ = 0
@[simp]
theorem Quaternion.ratCast_imK {R : Type u_1} (q : ) :
(↑q).imK = 0
@[deprecated Quaternion.ratCast_imI]
theorem Quaternion.rat_cast_imI {R : Type u_1} (q : ) :
(↑q).imI = 0

Alias of Quaternion.ratCast_imI.

@[deprecated Quaternion.ratCast_imJ]
theorem Quaternion.rat_cast_imJ {R : Type u_1} (q : ) :
(↑q).imJ = 0

Alias of Quaternion.ratCast_imJ.

@[deprecated Quaternion.ratCast_imK]
theorem Quaternion.rat_cast_imK {R : Type u_1} (q : ) :
(↑q).imK = 0

Alias of Quaternion.ratCast_imK.

theorem Quaternion.coe_nnratCast {R : Type u_1} (q : ℚ≥0) :
q = q
theorem Quaternion.coe_ratCast {R : Type u_1} (q : ) :
q = q
@[deprecated Quaternion.coe_ratCast]
theorem Quaternion.coe_rat_cast {R : Type u_1} (q : ) :
q = q

Alias of Quaternion.coe_ratCast.

instance Quaternion.instDivisionRing {R : Type u_1} :
Equations
• One or more equations did not get rendered due to their size.
theorem Quaternion.normSq_inv {R : Type u_1} (a : ) :
Quaternion.normSq a⁻¹ = (Quaternion.normSq a)⁻¹
theorem Quaternion.normSq_div {R : Type u_1} (a : ) (b : ) :
Quaternion.normSq (a / b) = Quaternion.normSq a / Quaternion.normSq b
theorem Quaternion.normSq_zpow {R : Type u_1} (a : ) (z : ) :
Quaternion.normSq (a ^ z) = Quaternion.normSq a ^ z
theorem Quaternion.normSq_ratCast {R : Type u_1} (q : ) :
(Quaternion.normSq q) = q ^ 2
@[deprecated Quaternion.normSq_ratCast]
theorem Quaternion.normSq_rat_cast {R : Type u_1} (q : ) :
(Quaternion.normSq q) = q ^ 2

Alias of Quaternion.normSq_ratCast.

theorem Cardinal.mk_quaternionAlgebra {R : Type u_1} (c₁ : R) (c₂ : R) :

The cardinality of a quaternion algebra, as a type.

@[simp]
theorem Cardinal.mk_quaternionAlgebra_of_infinite {R : Type u_1} (c₁ : R) (c₂ : R) [] :
theorem Cardinal.mk_univ_quaternionAlgebra {R : Type u_1} (c₁ : R) (c₂ : R) :
Cardinal.mk Set.univ = ^ 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) [] :
Cardinal.mk Set.univ =
instance Cardinal.instReprQuaternionAlgebra {R : Type u_1} [Repr R] {a : R} {b : R} :

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] :
= ^ 4

The cardinality of the quaternions, as a type.

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

The cardinality of the quaternions, as a set.

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