# mathlibdocumentation

algebra.quaternion

# Quaternions #

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

## Main definitions #

• `quaternion_algebra R a b`, `ℍ[R, a, b]` : quaternion algebra with coefficients `a`, `b`
• `quaternion R`, `ℍ[R]` : the space of quaternions, a.k.a. `quaternion_algebra R (-1) (-1)`;
• `quaternion.norm_sq` : square of the norm of a quaternion;
• `quaternion.conj` : conjugate of a quaternion;

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

• `ring ℍ[R, a, b]` and `algebra R ℍ[R, a, b]` : for any commutative ring `R`;
• `ring ℍ[R]` and `algebra R ℍ[R]` : for any commutative ring `R`;
• `domain ℍ[R]` : for a linear ordered commutative ring `R`;
• `division_algebra ℍ[R]` : for a linear ordered field `R`.

## Notation #

The following notation is available with `open_locale quaternion`.

• `ℍ[R, c₁, c₂]` : `quaternion_algebra 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 quaternion_algebra.ext {R : Type u_1} {a b : R} (x y : b) (h : x.re = y.re) (h_1 : x.im_i = y.im_i) (h_2 : x.im_j = y.im_j) (h_3 : x.im_k = y.im_k) :
x = y
theorem quaternion_algebra.ext_iff {R : Type u_1} {a b : R} (x y : b) :
x = y x.re = y.re x.im_i = y.im_i x.im_j = y.im_j x.im_k = y.im_k
@[nolint, ext]
structure quaternion_algebra (R : Type u_1) (a b : R) :
Type u_1
• re : R
• im_i : R
• im_j : R
• im_k : R

Quaternion algebra over a type with fixed coefficients \$a=i^2\$ and \$b=j^2\$. Implemented as a structure with four fields: `re`, `im_i`, `im_j`, and `im_k`.

Instances for `quaternion_algebra`
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_re {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
( c₂).symm) a).re = a.fst
@[simp]
theorem quaternion_algebra.equiv_prod_apply {R : Type u_1} (c₁ c₂ : R) (a : c₂) :
a = (a.re, a.im_i, a.im_j, a.im_k)
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_im_i {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
( c₂).symm) a).im_i = a.snd.fst
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_im_j {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
( c₂).symm) a).im_j = a.snd.snd.fst
def quaternion_algebra.equiv_prod {R : Type u_1} (c₁ c₂ : R) :
c₂ R × R × R × R

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

Equations
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_im_k {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
( c₂).symm) a).im_k = a.snd.snd.snd
@[simp]
theorem quaternion_algebra.mk.eta {R : Type u_1} {c₁ c₂ : R} (a : c₂) :
{re := a.re, im_i := a.im_i, im_j := a.im_j, im_k := a.im_k} = a
@[protected, instance]
def quaternion_algebra.has_coe_t {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.coe_re {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
x.re = x
@[simp]
theorem quaternion_algebra.coe_im_i {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
@[simp]
theorem quaternion_algebra.coe_im_j {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
@[simp]
theorem quaternion_algebra.coe_im_k {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
theorem quaternion_algebra.coe_injective {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
@[simp]
theorem quaternion_algebra.coe_inj {R : Type u_1} [comm_ring R] {c₁ c₂ x y : R} :
x = y x = y
@[simp]
theorem quaternion_algebra.has_zero_zero_re {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
0.re = 0
@[simp]
theorem quaternion_algebra.has_zero_zero_im_i {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
0.im_i = 0
@[protected, instance]
def quaternion_algebra.has_zero {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
has_zero c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.has_zero_zero_im_k {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
0.im_k = 0
@[simp]
theorem quaternion_algebra.has_zero_zero_im_j {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
0.im_j = 0
@[simp, norm_cast]
theorem quaternion_algebra.coe_zero {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
0 = 0
@[protected, instance]
def quaternion_algebra.inhabited {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
inhabited c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.has_one_one_im_i {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
1.im_i = 0
@[protected, instance]
def quaternion_algebra.has_one {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
has_one c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.has_one_one_im_j {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
1.im_j = 0
@[simp]
theorem quaternion_algebra.has_one_one_im_k {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
1.im_k = 0
@[simp]
theorem quaternion_algebra.has_one_one_re {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
1.re = 1
@[simp, norm_cast]
theorem quaternion_algebra.coe_one {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
1 = 1
@[simp]
theorem quaternion_algebra.has_add_add_im_k {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
(a + b).im_k = a.im_k + b.im_k
@[simp]
theorem quaternion_algebra.has_add_add_im_i {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
(a + b).im_i = a.im_i + b.im_i
@[simp]
theorem quaternion_algebra.has_add_add_im_j {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
(a + b).im_j = a.im_j + b.im_j
@[protected, instance]
def quaternion_algebra.has_add {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
Equations
@[simp]
theorem quaternion_algebra.has_add_add_re {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
(a + b).re = a.re + b.re
@[simp]
theorem quaternion_algebra.mk_add_mk {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) :
{re := a₁, im_i := a₂, im_j := a₃, im_k := a₄} + {re := b₁, im_i := b₂, im_j := b₃, im_k := b₄} = {re := a₁ + b₁, im_i := a₂ + b₂, im_j := a₃ + b₃, im_k := a₄ + b₄}
@[simp, norm_cast]
theorem quaternion_algebra.coe_add {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x y : R) :
(x + y) = x + y
@[protected, instance]
def quaternion_algebra.has_neg {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
has_neg c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.has_neg_neg_im_i {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
(-a).im_i = -a.im_i
@[simp]
theorem quaternion_algebra.has_neg_neg_re {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
(-a).re = -a.re
@[simp]
theorem quaternion_algebra.has_neg_neg_im_j {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
(-a).im_j = -a.im_j
@[simp]
theorem quaternion_algebra.has_neg_neg_im_k {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
(-a).im_k = -a.im_k
@[simp]
theorem quaternion_algebra.neg_mk {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a₁ a₂ a₃ a₄ : R) :
-{re := a₁, im_i := a₂, im_j := a₃, im_k := a₄} = {re := -a₁, im_i := -a₂, im_j := -a₃, im_k := -a₄}
@[simp, norm_cast]
theorem quaternion_algebra.coe_neg {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
@[simp]
theorem quaternion_algebra.has_sub_sub_im_k {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
(a - b).im_k = a.im_k - b.im_k
@[simp]
theorem quaternion_algebra.has_sub_sub_im_j {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
(a - b).im_j = a.im_j - b.im_j
@[protected, instance]
def quaternion_algebra.has_sub {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
has_sub c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.has_sub_sub_im_i {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
(a - b).im_i = a.im_i - b.im_i
@[simp]
theorem quaternion_algebra.has_sub_sub_re {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
(a - b).re = a.re - b.re
@[simp]
theorem quaternion_algebra.mk_sub_mk {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) :
{re := a₁, im_i := a₂, im_j := a₃, im_k := a₄} - {re := b₁, im_i := b₂, im_j := b₃, im_k := b₄} = {re := a₁ - b₁, im_i := a₂ - b₂, im_j := a₃ - b₃, im_k := a₄ - b₄}
@[simp]
theorem quaternion_algebra.has_mul_mul_im_k {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
(a * b).im_k = a.re * b.im_k + a.im_i * b.im_j - a.im_j * b.im_i + a.im_k * b.re
@[simp]
theorem quaternion_algebra.has_mul_mul_re {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
(a * b).re = a.re * b.re + c₁ * a.im_i * b.im_i + c₂ * a.im_j * b.im_j - c₁ * c₂ * a.im_k * b.im_k
@[protected, instance]
def quaternion_algebra.has_mul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
has_mul 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
@[simp]
theorem quaternion_algebra.has_mul_mul_im_j {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
(a * b).im_j = a.re * b.im_j + c₁ * a.im_i * b.im_k + a.im_j * b.re - c₁ * a.im_k * b.im_i
@[simp]
theorem quaternion_algebra.has_mul_mul_im_i {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
(a * b).im_i = a.re * b.im_i + a.im_i * b.re - c₂ * a.im_j * b.im_k + c₂ * a.im_k * b.im_j
@[simp]
theorem quaternion_algebra.mk_mul_mk {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) :
{re := a₁, im_i := a₂, im_j := a₃, im_k := a₄} * {re := b₁, im_i := b₂, im_j := b₃, im_k := b₄} = {re := a₁ * b₁ + c₁ * a₂ * b₂ + c₂ * a₃ * b₃ - c₁ * c₂ * a₄ * b₄, im_i := a₁ * b₂ + a₂ * b₁ - c₂ * a₃ * b₄ + c₂ * a₄ * b₃, im_j := a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ - c₁ * a₄ * b₂, im_k := a₁ * b₄ + a₂ * b₃ - a₃ * b₂ + a₄ * b₁}
@[protected, instance]
def quaternion_algebra.add_comm_group {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
Equations
@[protected, instance]
def quaternion_algebra.add_group_with_one {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
Equations
@[protected, instance]
def quaternion_algebra.ring {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
ring c₁ c₂)
Equations
@[protected, instance]
def quaternion_algebra.algebra {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.smul_re {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : c₂) :
(r a).re = r a.re
@[simp]
theorem quaternion_algebra.smul_im_i {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : c₂) :
(r a).im_i = r a.im_i
@[simp]
theorem quaternion_algebra.smul_im_j {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : c₂) :
(r a).im_j = r a.im_j
@[simp]
theorem quaternion_algebra.smul_im_k {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : c₂) :
(r a).im_k = r a.im_k
@[simp]
theorem quaternion_algebra.smul_mk {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r re im_i im_j im_k : R) :
r {re := re, im_i := im_i, im_j := im_j, im_k := im_k} = {re := r re, im_i := r im_i, im_j := r im_j, im_k := r im_k}
theorem quaternion_algebra.algebra_map_eq {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) :
c₁ c₂)) r = {re := r, im_i := 0, im_j := 0, im_k := 0}
def quaternion_algebra.re_lm (R : Type u_1) [comm_ring R] (c₁ c₂ : R) :
c₂ →ₗ[R] R

`quaternion_algebra.re` as a `linear_map`

Equations
@[simp]
theorem quaternion_algebra.re_lm_apply (R : Type u_1) [comm_ring R] (c₁ c₂ : R) (self : c₂) :
c₂) self = self.re
def quaternion_algebra.im_i_lm (R : Type u_1) [comm_ring R] (c₁ c₂ : R) :
c₂ →ₗ[R] R

`quaternion_algebra.im_i` as a `linear_map`

Equations
@[simp]
theorem quaternion_algebra.im_i_lm_apply (R : Type u_1) [comm_ring R] (c₁ c₂ : R) (self : c₂) :
c₂) self = self.im_i
@[simp]
theorem quaternion_algebra.im_j_lm_apply (R : Type u_1) [comm_ring R] (c₁ c₂ : R) (self : c₂) :
c₂) self = self.im_j
def quaternion_algebra.im_j_lm (R : Type u_1) [comm_ring R] (c₁ c₂ : R) :
c₂ →ₗ[R] R

`quaternion_algebra.im_j` as a `linear_map`

Equations
@[simp]
theorem quaternion_algebra.im_k_lm_apply (R : Type u_1) [comm_ring R] (c₁ c₂ : R) (self : c₂) :
c₂) self = self.im_k
def quaternion_algebra.im_k_lm (R : Type u_1) [comm_ring R] (c₁ c₂ : R) :
c₂ →ₗ[R] R

`quaternion_algebra.im_k` as a `linear_map`

Equations
@[simp, norm_cast]
theorem quaternion_algebra.coe_sub {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x y : R) :
(x - y) = x - y
@[simp, norm_cast]
theorem quaternion_algebra.coe_mul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x y : R) :
(x * y) = x * y
theorem quaternion_algebra.coe_commutes {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : c₂) :
r * a = a * r
theorem quaternion_algebra.coe_commute {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : c₂) :
a
theorem quaternion_algebra.coe_mul_eq_smul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : c₂) :
r * a = r a
theorem quaternion_algebra.mul_coe_eq_smul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : c₂) :
a * r = r a
@[simp, norm_cast]
theorem quaternion_algebra.coe_algebra_map {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
c₁ c₂)) = coe
theorem quaternion_algebra.smul_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x y : R) :
x y = (x * y)
def quaternion_algebra.conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
c₂ ≃ₗ[R] c₂

Quaternion conjugate.

Equations
@[simp]
theorem quaternion_algebra.re_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
@[simp]
theorem quaternion_algebra.im_i_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
@[simp]
theorem quaternion_algebra.im_j_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
@[simp]
theorem quaternion_algebra.im_k_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
@[simp]
theorem quaternion_algebra.conj_mk {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a₁ a₂ a₃ a₄ : R) :
quaternion_algebra.conj {re := a₁, im_i := a₂, im_j := a₃, im_k := a₄} = {re := a₁, im_i := -a₂, im_j := -a₃, im_k := -a₄}
@[simp]
theorem quaternion_algebra.conj_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
theorem quaternion_algebra.conj_add {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
@[simp]
theorem quaternion_algebra.conj_mul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
theorem quaternion_algebra.conj_conj_mul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
theorem quaternion_algebra.conj_mul_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
theorem quaternion_algebra.self_add_conj' {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= (2 * a.re)
theorem quaternion_algebra.self_add_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= 2 * (a.re)
theorem quaternion_algebra.conj_add_self' {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= (2 * a.re)
theorem quaternion_algebra.conj_add_self {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= 2 * (a.re)
theorem quaternion_algebra.conj_eq_two_re_sub {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= (2 * a.re) - a
theorem quaternion_algebra.commute_conj_self {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
theorem quaternion_algebra.commute_self_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
theorem quaternion_algebra.commute_conj_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} {a b : c₂} (h : b) :
@[simp]
theorem quaternion_algebra.conj_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
theorem quaternion_algebra.conj_smul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : c₂) :
@[simp]
theorem quaternion_algebra.conj_one {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
theorem quaternion_algebra.eq_re_of_eq_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} {a : c₂} {x : R} (h : a = x) :
a = (a.re)
theorem quaternion_algebra.eq_re_iff_mem_range_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} {a : c₂} :
a = (a.re)
@[simp]
theorem quaternion_algebra.conj_fixed {R : Type u_1} [comm_ring R] [char_zero R] {c₁ c₂ : R} {a : c₂} :
a = (a.re)
theorem quaternion_algebra.conj_mul_eq_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= .re)
theorem quaternion_algebra.mul_conj_eq_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= .re)
theorem quaternion_algebra.conj_zero {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
theorem quaternion_algebra.conj_neg {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
theorem quaternion_algebra.conj_sub {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : c₂) :
@[protected, instance]
def quaternion_algebra.star_ring {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
star_ring c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.star_def {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
def quaternion_algebra.conj_ae {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
c₂ ≃ₐ[R] c₁ c₂)ᵐᵒᵖ

Quaternion conjugate as an `alg_equiv` to the opposite ring.

Equations
@[simp]
theorem quaternion_algebra.coe_conj_ae {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
def quaternion (R : Type u_1) [has_one R] [has_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
• = (-1) (-1)
Instances for `quaternion`
def quaternion.equiv_prod (R : Type u_1) [has_one R] [has_neg R] :
R × R × R × R

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

Equations
@[protected, instance]
def quaternion.has_coe_t {R : Type u_1} [comm_ring R] :
Equations
@[protected, instance]
def quaternion.ring {R : Type u_1} [comm_ring R] :
Equations
@[protected, instance]
def quaternion.inhabited {R : Type u_1} [comm_ring R] :
Equations
@[protected, instance]
def quaternion.algebra {R : Type u_1} [comm_ring R] :
Equations
@[protected, instance]
def quaternion.star_ring {R : Type u_1} [comm_ring R] :
Equations
@[ext]
theorem quaternion.ext {R : Type u_1} [comm_ring R] (a b : quaternion R) :
a.re = b.rea.im_i = b.im_ia.im_j = b.im_ja.im_k = b.im_ka = b
theorem quaternion.ext_iff {R : Type u_1} [comm_ring R] {a b : quaternion R} :
a = b a.re = b.re a.im_i = b.im_i a.im_j = b.im_j a.im_k = b.im_k
@[simp, norm_cast]
theorem quaternion.coe_re {R : Type u_1} [comm_ring R] (x : R) :
x.re = x
@[simp, norm_cast]
theorem quaternion.coe_im_i {R : Type u_1} [comm_ring R] (x : R) :
@[simp, norm_cast]
theorem quaternion.coe_im_j {R : Type u_1} [comm_ring R] (x : R) :
@[simp, norm_cast]
theorem quaternion.coe_im_k {R : Type u_1} [comm_ring R] (x : R) :
@[simp]
theorem quaternion.zero_re {R : Type u_1} [comm_ring R] :
0.re = 0
@[simp]
theorem quaternion.zero_im_i {R : Type u_1} [comm_ring R] :
0.im_i = 0
@[simp]
theorem quaternion.zero_im_j {R : Type u_1} [comm_ring R] :
0.im_j = 0
@[simp]
theorem quaternion.zero_im_k {R : Type u_1} [comm_ring R] :
0.im_k = 0
@[simp, norm_cast]
theorem quaternion.coe_zero {R : Type u_1} [comm_ring R] :
0 = 0
@[simp]
theorem quaternion.one_re {R : Type u_1} [comm_ring R] :
1.re = 1
@[simp]
theorem quaternion.one_im_i {R : Type u_1} [comm_ring R] :
1.im_i = 0
@[simp]
theorem quaternion.one_im_j {R : Type u_1} [comm_ring R] :
1.im_j = 0
@[simp]
theorem quaternion.one_im_k {R : Type u_1} [comm_ring R] :
1.im_k = 0
@[simp, norm_cast]
theorem quaternion.coe_one {R : Type u_1} [comm_ring R] :
1 = 1
@[simp]
theorem quaternion.add_re {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a + b).re = a.re + b.re
@[simp]
theorem quaternion.add_im_i {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a + b).im_i = a.im_i + b.im_i
@[simp]
theorem quaternion.add_im_j {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a + b).im_j = a.im_j + b.im_j
@[simp]
theorem quaternion.add_im_k {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a + b).im_k = a.im_k + b.im_k
@[simp, norm_cast]
theorem quaternion.coe_add {R : Type u_1} [comm_ring R] (x y : R) :
(x + y) = x + y
@[simp]
theorem quaternion.neg_re {R : Type u_1} [comm_ring R] (a : quaternion R) :
(-a).re = -a.re
@[simp]
theorem quaternion.neg_im_i {R : Type u_1} [comm_ring R] (a : quaternion R) :
(-a).im_i = -a.im_i
@[simp]
theorem quaternion.neg_im_j {R : Type u_1} [comm_ring R] (a : quaternion R) :
(-a).im_j = -a.im_j
@[simp]
theorem quaternion.neg_im_k {R : Type u_1} [comm_ring R] (a : quaternion R) :
(-a).im_k = -a.im_k
@[simp, norm_cast]
theorem quaternion.coe_neg {R : Type u_1} [comm_ring R] (x : R) :
@[simp]
theorem quaternion.sub_re {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a - b).re = a.re - b.re
@[simp]
theorem quaternion.sub_im_i {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a - b).im_i = a.im_i - b.im_i
@[simp]
theorem quaternion.sub_im_j {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a - b).im_j = a.im_j - b.im_j
@[simp]
theorem quaternion.sub_im_k {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a - b).im_k = a.im_k - b.im_k
@[simp, norm_cast]
theorem quaternion.coe_sub {R : Type u_1} [comm_ring R] (x y : R) :
(x - y) = x - y
@[simp]
theorem quaternion.mul_re {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a * b).re = a.re * b.re - a.im_i * b.im_i - a.im_j * b.im_j - a.im_k * b.im_k
@[simp]
theorem quaternion.mul_im_i {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a * b).im_i = a.re * b.im_i + a.im_i * b.re + a.im_j * b.im_k - a.im_k * b.im_j
@[simp]
theorem quaternion.mul_im_j {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a * b).im_j = a.re * b.im_j - a.im_i * b.im_k + a.im_j * b.re + a.im_k * b.im_i
@[simp]
theorem quaternion.mul_im_k {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a * b).im_k = a.re * b.im_k + a.im_i * b.im_j - a.im_j * b.im_i + a.im_k * b.re
@[simp, norm_cast]
theorem quaternion.coe_mul {R : Type u_1} [comm_ring R] (x y : R) :
(x * y) = x * y
theorem quaternion.coe_injective {R : Type u_1} [comm_ring R] :
@[simp]
theorem quaternion.coe_inj {R : Type u_1} [comm_ring R] {x y : R} :
x = y x = y
@[simp]
theorem quaternion.smul_re {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
(r a).re = r a.re
@[simp]
theorem quaternion.smul_im_i {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
(r a).im_i = r a.im_i
@[simp]
theorem quaternion.smul_im_j {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
(r a).im_j = r a.im_j
@[simp]
theorem quaternion.smul_im_k {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
(r a).im_k = r a.im_k
theorem quaternion.coe_commutes {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
r * a = a * r
theorem quaternion.coe_commute {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
a
theorem quaternion.coe_mul_eq_smul {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
r * a = r a
theorem quaternion.mul_coe_eq_smul {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
a * r = r a
@[simp]
theorem quaternion.algebra_map_def {R : Type u_1} [comm_ring R] :
theorem quaternion.smul_coe {R : Type u_1} [comm_ring R] (x y : R) :
x y = (x * y)
def quaternion.conj {R : Type u_1} [comm_ring R] :

Quaternion conjugate.

Equations
@[simp]
theorem quaternion.conj_re {R : Type u_1} [comm_ring R] (a : quaternion R) :
.re = a.re
@[simp]
theorem quaternion.conj_im_i {R : Type u_1} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.conj_im_j {R : Type u_1} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.conj_im_k {R : Type u_1} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.conj_conj {R : Type u_1} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.conj_add {R : Type u_1} [comm_ring R] (a b : quaternion R) :
@[simp]
theorem quaternion.conj_mul {R : Type u_1} [comm_ring R] (a b : quaternion R) :
theorem quaternion.conj_conj_mul {R : Type u_1} [comm_ring R] (a b : quaternion R) :
=
theorem quaternion.conj_mul_conj {R : Type u_1} [comm_ring R] (a b : quaternion R) :
=
theorem quaternion.self_add_conj' {R : Type u_1} [comm_ring R] (a : quaternion R) :
= (2 * a.re)
theorem quaternion.self_add_conj {R : Type u_1} [comm_ring R] (a : quaternion R) :
= 2 * (a.re)
theorem quaternion.conj_add_self' {R : Type u_1} [comm_ring R] (a : quaternion R) :
= (2 * a.re)
theorem quaternion.conj_add_self {R : Type u_1} [comm_ring R] (a : quaternion R) :
= 2 * (a.re)
theorem quaternion.conj_eq_two_re_sub {R : Type u_1} [comm_ring R] (a : quaternion R) :
= (2 * a.re) - a
theorem quaternion.commute_conj_self {R : Type u_1} [comm_ring R] (a : quaternion R) :
a
theorem quaternion.commute_self_conj {R : Type u_1} [comm_ring R] (a : quaternion R) :
theorem quaternion.commute_conj_conj {R : Type u_1} [comm_ring R] {a b : quaternion R} (h : b) :
theorem quaternion.commute.quaternion_conj {R : Type u_1} [comm_ring R] {a b : quaternion R} (h : b) :

Alias of `quaternion.commute_conj_conj`.

@[simp]
theorem quaternion.conj_coe {R : Type u_1} [comm_ring R] (x : R) :
@[simp]
theorem quaternion.conj_smul {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
@[simp]
theorem quaternion.conj_one {R : Type u_1} [comm_ring R] :
theorem quaternion.eq_re_of_eq_coe {R : Type u_1} [comm_ring R] {a : quaternion R} {x : R} (h : a = x) :
a = (a.re)
theorem quaternion.eq_re_iff_mem_range_coe {R : Type u_1} [comm_ring R] {a : quaternion R} :
a = (a.re)
@[simp]
theorem quaternion.conj_fixed {R : Type u_1} [comm_ring R] [char_zero R] {a : quaternion R} :
a = (a.re)
theorem quaternion.conj_mul_eq_coe {R : Type u_1} [comm_ring R] (a : quaternion R) :
= * a).re)
theorem quaternion.mul_conj_eq_coe {R : Type u_1} [comm_ring R] (a : quaternion R) :
= ((a * .re)
@[simp]
theorem quaternion.conj_zero {R : Type u_1} [comm_ring R] :
@[simp]
theorem quaternion.conj_neg {R : Type u_1} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.conj_sub {R : Type u_1} [comm_ring R] (a b : quaternion R) :
def quaternion.conj_ae {R : Type u_1} [comm_ring R] :

Quaternion conjugate as an `alg_equiv` to the opposite ring.

Equations
@[simp]
theorem quaternion.coe_conj_ae {R : Type u_1} [comm_ring R] :
def quaternion.norm_sq {R : Type u_1} [comm_ring R] :

Square of the norm.

Equations
theorem quaternion.norm_sq_def {R : Type u_1} [comm_ring R] (a : quaternion R) :
= (a * .re
theorem quaternion.norm_sq_def' {R : Type u_1} [comm_ring R] (a : quaternion R) :
= a.re ^ 2 + a.im_i ^ 2 + a.im_j ^ 2 + a.im_k ^ 2
theorem quaternion.norm_sq_coe {R : Type u_1} [comm_ring R] (x : R) :
= x ^ 2
@[simp]
theorem quaternion.norm_sq_neg {R : Type u_1} [comm_ring R] (a : quaternion R) :
theorem quaternion.self_mul_conj {R : Type u_1} [comm_ring R] (a : quaternion R) :
theorem quaternion.conj_mul_self {R : Type u_1} [comm_ring R] (a : quaternion R) :
theorem quaternion.coe_norm_sq_add {R : Type u_1} [comm_ring R] (a b : quaternion R) :
@[simp]
theorem quaternion.norm_sq_eq_zero {R : Type u_1} {a : quaternion R} :
a = 0
theorem quaternion.norm_sq_ne_zero {R : Type u_1} {a : quaternion R} :
a 0
@[simp]
theorem quaternion.norm_sq_nonneg {R : Type u_1} {a : quaternion R} :
@[simp]
theorem quaternion.norm_sq_le_zero {R : Type u_1} {a : quaternion R} :
a = 0
@[protected, instance]
def quaternion.nontrivial {R : Type u_1}  :
@[protected, instance]
def quaternion.is_domain {R : Type u_1}  :
@[protected, instance]
def quaternion.has_inv {R : Type u_1}  :
Equations
theorem quaternion.has_inv_inv {R : Type u_1} (a : quaternion R) :
@[protected, instance]
def quaternion.division_ring {R : Type u_1}  :
Equations
@[simp]
theorem quaternion.norm_sq_inv {R : Type u_1} (a : quaternion R) :
@[simp]
theorem quaternion.norm_sq_div {R : Type u_1} (a b : quaternion R) :
theorem cardinal.mk_quaternion_algebra {R : Type u_1} (c₁ c₂ : R) :
cardinal.mk c₁ c₂) = ^ 4

The cardinality of a quaternion algebra, as a type.

@[simp]
theorem cardinal.mk_quaternion_algebra_of_infinite {R : Type u_1} (c₁ c₂ : R) [infinite R] :
cardinal.mk c₁ c₂) =
theorem cardinal.mk_univ_quaternion_algebra {R : Type u_1} (c₁ c₂ : R) :

The cardinality of a quaternion algebra, as a set.

@[simp]
theorem cardinal.mk_univ_quaternion_algebra_of_infinite {R : Type u_1} (c₁ c₂ : R) [infinite R] :
@[simp]
theorem cardinal.mk_quaternion (R : Type u_1) [has_one R] [has_neg R] :
= ^ 4

The cardinality of the quaternions, as a type.

@[simp]
theorem cardinal.mk_quaternion_of_infinite (R : Type u_1) [has_one R] [has_neg R] [infinite R] :
@[simp]
theorem cardinal.mk_univ_quaternion (R : Type u_1) [has_one R] [has_neg R] :

The cardinality of the quaternions, as a set.

@[simp]
theorem cardinal.mk_univ_quaternion_of_infinite (R : Type u_1) [has_one R] [has_neg R] [infinite R] :