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

source

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

source

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

source

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

source

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

Lean.ParserDescr

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

Equations

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

Instances For

source

@[simp]

theorem QuaternionAlgebra.equivProd_symm_apply_re {R : Type u_1} (c₁ : R) (c₂ : R) (a : R × R × R × R) :

((QuaternionAlgebra.equivProd c₁ c₂).symm a).re = a.1

source

@[simp]

theorem QuaternionAlgebra.equivProd_symm_apply_imJ {R : Type u_1} (c₁ : R) (c₂ : R) (a : R × R × R × R) :

((QuaternionAlgebra.equivProd c₁ c₂).symm a).imJ = a.2.2.1

source

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

source

@[simp]

theorem QuaternionAlgebra.equivProd_symm_apply_imK {R : Type u_1} (c₁ : R) (c₂ : R) (a : R × R × R × R) :

((QuaternionAlgebra.equivProd c₁ c₂).symm a).imK = a.2.2.2

source

@[simp]

theorem QuaternionAlgebra.equivProd_symm_apply_imI {R : Type u_1} (c₁ : R) (c₂ : R) (a : R × R × R × R) :

((QuaternionAlgebra.equivProd c₁ c₂).symm a).imI = a.2.1

source

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

source

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

source

def QuaternionAlgebra.equivTuple {R : Type u_1} (c₁ : R) (c₂ : R) :

QuaternionAlgebra R c₁ c₂ ≃ (Fin 4 → R)

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

Equations

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

Instances For

source

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

source

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

source

instance QuaternionAlgebra.instSubsingletonQuaternionAlgebra {R : Type u_3} {c₁ : R} {c₂ : R} [Subsingleton R] :

Subsingleton (QuaternionAlgebra R c₁ c₂)

Equations

⋯ = ⋯

source

instance QuaternionAlgebra.instNontrivialQuaternionAlgebra {R : Type u_3} {c₁ : R} {c₂ : R} [Nontrivial R] :

Nontrivial (QuaternionAlgebra R c₁ c₂)

Equations

⋯ = ⋯

source

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

QuaternionAlgebra R c₁ c₂

The imaginary part of a quaternion.

Equations

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

QuaternionAlgebra R c₁ c₂

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

Equations

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

Instances For

source

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

CoeTC R (QuaternionAlgebra R c₁ c₂)

Equations

QuaternionAlgebra.instCoeTCQuaternionAlgebra = { coe := QuaternionAlgebra.coe }

source

@[simp]

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

(↑x).re = x

source

@[simp]

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

(↑x).imI = 0

source

@[simp]

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

(↑x).imJ = 0

source

@[simp]

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

(↑x).imK = 0

source

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

Function.Injective QuaternionAlgebra.coe

source

@[simp]

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

↑x = ↑y ↔ x = y

source

instance QuaternionAlgebra.instZeroQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :

Zero (QuaternionAlgebra R c₁ c₂)

Equations

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

source

@[simp]

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

0.re = 0

source

@[simp]

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

0.imI = 0

source

@[simp]

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

0.imJ = 0

source

@[simp]

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

0.imK = 0

source

@[simp]

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

QuaternionAlgebra.im 0 = 0

source

@[simp]

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

↑0 = 0

source

instance QuaternionAlgebra.instInhabitedQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :

Inhabited (QuaternionAlgebra R c₁ c₂)

Equations

QuaternionAlgebra.instInhabitedQuaternionAlgebra = { default := 0 }

source

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

One (QuaternionAlgebra R c₁ c₂)

Equations

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

source

@[simp]

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

1.re = 1

source

@[simp]

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

1.imI = 0

source

@[simp]

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

1.imJ = 0

source

@[simp]

theorem QuaternionAlgebra.one_imK {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :

1.imK = 0

source

@[simp]

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

QuaternionAlgebra.im 1 = 0

source

@[simp]

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

↑1 = 1

source

instance QuaternionAlgebra.instAddQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :

Add (QuaternionAlgebra R c₁ c₂)

Equations

QuaternionAlgebra.instAddQuaternionAlgebra = { 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 } }

source

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

source

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

source

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

source

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

source

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

source

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

source

@[simp]

theorem QuaternionAlgebra.coe_add {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} (x : R) (y : R) :

↑(x + y) = ↑x + ↑y

source

instance QuaternionAlgebra.instNegQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :

Neg (QuaternionAlgebra R c₁ c₂)

Equations

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

source

@[simp]

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

(-a).re = -a.re

source

@[simp]

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

(-a).imI = -a.imI

source

@[simp]

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

(-a).imJ = -a.imJ

source

@[simp]

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

(-a).imK = -a.imK

source

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

source

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

source

@[simp]

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

↑(-x) = -↑x

source

instance QuaternionAlgebra.instSubQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :

Sub (QuaternionAlgebra R c₁ c₂)

Equations

QuaternionAlgebra.instSubQuaternionAlgebra = { 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 } }

source

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

source

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

source

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

source

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

source

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

source

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

source

@[simp]

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

QuaternionAlgebra.im ↑x = 0

source

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

source

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

source

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

source

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.

Equations

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

source

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

source

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

source

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

source

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

source

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

source

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

SMul S (QuaternionAlgebra R c₁ c₂)

Equations

QuaternionAlgebra.instSMulQuaternionAlgebra = { 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 } }

source

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

Equations

⋯ = ⋯

source

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

Equations

⋯ = ⋯

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

instance QuaternionAlgebra.instAddCommGroupQuaternionAlgebra {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :

AddCommGroup (QuaternionAlgebra R c₁ c₂)

Equations

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

source

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

AddCommGroupWithOne (QuaternionAlgebra R c₁ c₂)

Equations

QuaternionAlgebra.instAddCommGroupWithOneQuaternionAlgebra = AddCommGroupWithOne.mk ⋯ ⋯ ⋯ ⋯

source

@[simp]

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

(↑n).re = ↑n

source

@[simp]

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

(↑n).imI = 0

source

@[simp]

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

(↑n).imJ = 0

source

@[simp]

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

(↑n).imK = 0

source

@[simp]

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

QuaternionAlgebra.im ↑n = 0

source

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

↑↑n = ↑n

source

@[simp]

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

(↑z).re = ↑z

source

@[simp]

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

(↑z).imI = 0

source

@[simp]

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

(↑z).imJ = 0

source

@[simp]

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

(↑z).imK = 0

source

@[simp]

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

QuaternionAlgebra.im ↑z = 0

source

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

↑↑z = ↑z

source

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

Ring (QuaternionAlgebra R c₁ c₂)

Equations

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

source

@[simp]

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

↑(x * y) = ↑x * ↑y

source

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

Equations

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

source

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 }

source

theorem QuaternionAlgebra.algebraMap_injective {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :

Function.Injective ⇑(algebraMap R (QuaternionAlgebra R c₁ c₂))

source

instance QuaternionAlgebra.instNoZeroSMulDivisorsQuaternionAlgebraToZeroToCommMonoidWithZeroToCommSemiringInstZeroQuaternionAlgebraInstSMulQuaternionAlgebraToSMulToSemiringId {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} [NoZeroDivisors R] :

NoZeroSMulDivisors R (QuaternionAlgebra R c₁ c₂)

Equations

⋯ = ⋯

source

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

source

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

QuaternionAlgebra R c₁ c₂ →ₗ[R] R

QuaternionAlgebra.re as a LinearMap

Equations

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

Instances For

source

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

source

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

QuaternionAlgebra R c₁ c₂ →ₗ[R] R

QuaternionAlgebra.imI as a LinearMap

Equations

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

Instances For

source

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

source

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

QuaternionAlgebra R c₁ c₂ →ₗ[R] R

QuaternionAlgebra.imJ as a LinearMap

Equations

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

Instances For

source

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

source

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

QuaternionAlgebra R c₁ c₂ →ₗ[R] R

QuaternionAlgebra.imK as a LinearMap

Equations

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

Instances For

source

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

QuaternionAlgebra R c₁ c₂ ≃ₗ[R] Fin 4 → R

QuaternionAlgebra.equivTuple as a linear equivalence.

Equations

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

Instances For

source

@[simp]

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

⇑(QuaternionAlgebra.linearEquivTuple c₁ c₂) = ⇑(QuaternionAlgebra.equivTuple c₁ c₂)

source

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

source

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

Basis (Fin 4) R (QuaternionAlgebra R c₁ c₂)

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

Equations

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

Instances For

source

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

source

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

Module.Finite R (QuaternionAlgebra R c₁ c₂)

Equations

⋯ = ⋯

source

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

Module.Free R (QuaternionAlgebra R c₁ c₂)

Equations

⋯ = ⋯

source

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

source

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

source

@[simp]

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

((QuaternionAlgebra.swapEquiv c₁ c₂) t).imI = t.imJ

source

@[simp]

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

((QuaternionAlgebra.swapEquiv c₁ c₂) t).imJ = t.imI

source

@[simp]

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

((AlgEquiv.symm (QuaternionAlgebra.swapEquiv c₁ c₂)) t).re = t.re

source

@[simp]

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

((QuaternionAlgebra.swapEquiv c₁ c₂) t).re = t.re

source

@[simp]

theorem QuaternionAlgebra.swapEquiv_symm_apply_imI {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₂ c₁) :

((AlgEquiv.symm (QuaternionAlgebra.swapEquiv c₁ c₂)) t).imI = t.imJ

source

@[simp]

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

((QuaternionAlgebra.swapEquiv c₁ c₂) t).imK = -t.imK

source

@[simp]

theorem QuaternionAlgebra.swapEquiv_symm_apply_imK {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₂ c₁) :

((AlgEquiv.symm (QuaternionAlgebra.swapEquiv c₁ c₂)) t).imK = -t.imK

source

@[simp]

theorem QuaternionAlgebra.swapEquiv_symm_apply_imJ {R : Type u_3} [CommRing R] (c₁ : R) (c₂ : R) (t : QuaternionAlgebra R c₂ c₁) :

((AlgEquiv.symm (QuaternionAlgebra.swapEquiv c₁ c₂)) t).imJ = t.imI

source

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

QuaternionAlgebra R c₁ c₂ ≃ₐ[R] QuaternionAlgebra R c₂ c₁

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

Equations

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

Instances For

source

@[simp]

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

↑(x - y) = ↑x - ↑y

source

@[simp]

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

↑(x ^ n) = ↑x ^ n

source

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

source

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

Commute (↑r) a

source

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

source

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

source

@[simp]

theorem QuaternionAlgebra.coe_algebraMap {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :

⇑(algebraMap R (QuaternionAlgebra R c₁ c₂)) = QuaternionAlgebra.coe

source

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

x • ↑y = ↑(x * y)

source

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

Star (QuaternionAlgebra R c₁ c₂)

Quaternion conjugate.

Equations

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

StarRing (QuaternionAlgebra R c₁ c₂)

Equations

QuaternionAlgebra.instStarRing = StarRing.mk ⋯

source

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)

source

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

source

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)

source

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

source

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

source

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

IsStarNormal a

Equations

⋯ = ⋯

source

@[simp]

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

star ↑x = ↑x

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

def QuaternionAlgebra.starAe {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :

QuaternionAlgebra R c₁ c₂ ≃ₐ[R] (QuaternionAlgebra R c₁ c₂)ᵐᵒᵖ

Quaternion conjugate as an AlgEquiv to the opposite ring.

Equations

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

Instances For

source

@[simp]

theorem QuaternionAlgebra.coe_starAe {R : Type u_3} [CommRing R] {c₁ : R} {c₂ : R} :

⇑QuaternionAlgebra.starAe = MulOpposite.op ∘ star

source

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

Type u_1

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

Equations

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

Instances For

source

def Quaternion.«termℍ[_]» :

Lean.ParserDescr

Equations

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

Instances For

source

@[simp]

theorem Quaternion.equivProd_symm_apply_imI (R : Type u_1) [One R] [Neg R] (a : R × R × R × R) :

((Quaternion.equivProd R).symm a).imI = a.2.1

source

@[simp]

theorem Quaternion.equivProd_symm_apply_re (R : Type u_1) [One R] [Neg R] (a : R × R × R × R) :

((Quaternion.equivProd R).symm a).re = a.1

source

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

source

@[simp]

theorem Quaternion.equivProd_symm_apply_imK (R : Type u_1) [One R] [Neg R] (a : R × R × R × R) :

((Quaternion.equivProd R).symm a).imK = a.2.2.2

source

@[simp]

theorem Quaternion.equivProd_symm_apply_imJ (R : Type u_1) [One R] [Neg R] (a : R × R × R × R) :

((Quaternion.equivProd R).symm a).imJ = a.2.2.1

source

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

Quaternion R ≃ R × R × R × R

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

Equations

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

Instances For

source

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

source

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

Quaternion R ≃ (Fin 4 → R)

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

Equations

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

Instances For

source

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

source

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

Subsingleton (Quaternion R)

Equations

⋯ = ⋯

source

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

Nontrivial (Quaternion R)

Equations

⋯ = ⋯

source

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

R → Quaternion R

Coercion R → ℍ[R].

Equations

Quaternion.coe = QuaternionAlgebra.coe

Instances For

source

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

CoeTC R (Quaternion R)

Equations

Quaternion.instCoeTCQuaternionToOneToSemiringToCommSemiringToNegToRing = { coe := Quaternion.coe }

source

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

Ring (Quaternion R)

Equations

Quaternion.instRing = QuaternionAlgebra.instRing

source

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

Inhabited (Quaternion R)

Equations

Quaternion.instInhabitedQuaternionToOneToSemiringToCommSemiringToNegToRing = inferInstanceAs (Inhabited (QuaternionAlgebra R (-1) (-1)))

source

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

SMul S (Quaternion R)

Equations

Quaternion.instSMulQuaternionToOneToSemiringToCommSemiringToNegToRing = inferInstanceAs (SMul S (QuaternionAlgebra R (-1) (-1)))

source

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)

Equations

⋯ = ⋯

source

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)

Equations

⋯ = ⋯

source

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

Algebra S (Quaternion R)

Equations

Quaternion.algebra = inferInstanceAs (Algebra S (QuaternionAlgebra R (-1) (-1)))

source

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

Star (Quaternion R)

Equations

Quaternion.instStarQuaternionToOneToSemiringToCommSemiringToNegToRing = QuaternionAlgebra.instStarQuaternionAlgebra

source

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

StarRing (Quaternion R)

Equations

Quaternion.instStarRingQuaternionToOneToSemiringToCommSemiringToNegToRingToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRing = QuaternionAlgebra.instStarRing

source