# mathlib3documentation

algebra.quaternion

# Quaternions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

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.

## 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.equiv_tuple_symm_apply {R : Type u_1} (c₁ c₂ : R) (a : fin 4 R) :
c₂).symm) a = {re := a 0, im_i := a 1, im_j := a 2, im_k := a 3}
def quaternion_algebra.equiv_tuple {R : Type u_1} (c₁ c₂ : R) :
c₂ (fin 4 R)

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

Equations
@[simp]
theorem quaternion_algebra.equiv_tuple_apply {R : Type u_1} (c₁ c₂ : R) (x : c₂) :
x = ![x.re, x.im_i, x.im_j, x.im_k]
@[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
def quaternion_algebra.im {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : c₂) :
c₂

The imaginary part of a quaternion.

Equations
@[simp]
theorem quaternion_algebra.im_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
a.im.re = 0
@[simp]
theorem quaternion_algebra.im_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
@[simp]
theorem quaternion_algebra.im_im_j {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
@[simp]
theorem quaternion_algebra.im_im_k {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
@[simp]
theorem quaternion_algebra.im_idem {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
a.im.im = a.im
@[protected, instance]
def quaternion_algebra.has_coe_t {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
c₁ c₂)
Equations
@[simp, norm_cast]
theorem quaternion_algebra.coe_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
x.re = x
@[simp, norm_cast]
theorem quaternion_algebra.coe_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
@[simp, norm_cast]
theorem quaternion_algebra.coe_im_j {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
@[simp, norm_cast]
theorem quaternion_algebra.coe_im_k {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
theorem quaternion_algebra.coe_injective {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
@[simp]
theorem quaternion_algebra.coe_inj {R : Type u_3} [comm_ring R] {c₁ c₂ x y : R} :
x = y x = y
@[simp]
theorem quaternion_algebra.has_zero_zero_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
0.re = 0
@[simp]
theorem quaternion_algebra.has_zero_zero_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
0.im_i = 0
@[protected, instance]
def quaternion_algebra.has_zero {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
has_zero c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.has_zero_zero_im_k {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
0.im_k = 0
@[simp]
theorem quaternion_algebra.has_zero_zero_im_j {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
0.im_j = 0
@[simp, norm_cast]
theorem quaternion_algebra.coe_zero {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
0 = 0
@[protected, instance]
def quaternion_algebra.inhabited {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
inhabited c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.has_one_one_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
1.im_i = 0
@[protected, instance]
def quaternion_algebra.has_one {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
has_one c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.has_one_one_im_j {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
1.im_j = 0
@[simp]
theorem quaternion_algebra.has_one_one_im_k {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
1.im_k = 0
@[simp]
theorem quaternion_algebra.has_one_one_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
1.re = 1
@[simp, norm_cast]
theorem quaternion_algebra.coe_one {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
1 = 1
@[simp]
theorem quaternion_algebra.has_add_add_im_k {R : Type u_3} [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_3} [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_3} [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_3} [comm_ring R] {c₁ c₂ : R} :
Equations
@[simp]
theorem quaternion_algebra.has_add_add_re {R : Type u_3} [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_3} [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_3} [comm_ring R] {c₁ c₂ : R} (x y : R) :
(x + y) = x + y
@[protected, instance]
def quaternion_algebra.has_neg {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
has_neg c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.has_neg_neg_im_i {R : Type u_3} [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_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
(-a).re = -a.re
@[simp]
theorem quaternion_algebra.has_neg_neg_im_j {R : Type u_3} [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_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
(-a).im_k = -a.im_k
@[simp]
theorem quaternion_algebra.neg_mk {R : Type u_3} [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_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
@[simp]
theorem quaternion_algebra.has_sub_sub_im_k {R : Type u_3} [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_3} [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_3} [comm_ring R] {c₁ c₂ : R} :
has_sub c₁ c₂)
Equations
@[simp]
theorem quaternion_algebra.has_sub_sub_im_i {R : Type u_3} [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_3} [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_3} [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_im {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
x.im = 0
@[simp]
theorem quaternion_algebra.re_add_im {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
(a.re) + a.im = a
@[simp]
theorem quaternion_algebra.sub_self_im {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
a - a.im = (a.re)
@[simp]
theorem quaternion_algebra.sub_self_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
a - (a.re) = a.im
@[simp]
theorem quaternion_algebra.has_mul_mul_im_k {R : Type u_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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, nolint, instance]
def quaternion_algebra.has_smul {S : Type u_1} {R : Type u_3} [comm_ring R] {c₁ c₂ : R} [ R] :
c₁ c₂)
Equations
@[protected, instance]
def quaternion_algebra.is_scalar_tower {S : Type u_1} {T : Type u_2} {R : Type u_3} [comm_ring R] {c₁ c₂ : R} [ R] [ R] [ T] [ R] :
c₁ c₂)
@[protected, instance]
def quaternion_algebra.smul_comm_class {S : Type u_1} {T : Type u_2} {R : Type u_3} [comm_ring R] {c₁ c₂ : R} [ R] [ R] [ R] :
c₁ c₂)
@[simp]
theorem quaternion_algebra.smul_re {S : Type u_1} {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) [ R] (s : S) :
(s a).re = s a.re
@[simp]
theorem quaternion_algebra.smul_im_i {S : Type u_1} {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) [ R] (s : S) :
(s a).im_i = s a.im_i
@[simp]
theorem quaternion_algebra.smul_im_j {S : Type u_1} {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) [ R] (s : S) :
(s a).im_j = s a.im_j
@[simp]
theorem quaternion_algebra.smul_im_k {S : Type u_1} {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) [ R] (s : S) :
(s a).im_k = s a.im_k
@[simp]
theorem quaternion_algebra.smul_mk {S : Type u_1} {R : Type u_3} [comm_ring R] {c₁ c₂ : R} [ R] (s : S) (re im_i im_j im_k : R) :
s {re := re, im_i := im_i, im_j := im_j, im_k := im_k} = {re := s re, im_i := s im_i, im_j := s im_j, im_k := s im_k}
@[simp, norm_cast]
theorem quaternion_algebra.coe_smul {S : Type u_1} {R : Type u_3} [comm_ring R] {c₁ c₂ : R} [ R] (s : S) (r : R) :
(s r) = s r
@[protected, instance]
def quaternion_algebra.add_comm_group {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
Equations
@[protected, instance]
def quaternion_algebra.add_group_with_one {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
Equations
@[simp, norm_cast]
theorem quaternion_algebra.nat_cast_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (n : ) :
@[simp, norm_cast]
theorem quaternion_algebra.nat_cast_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (n : ) :
@[simp, norm_cast]
theorem quaternion_algebra.nat_cast_im_j {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (n : ) :
@[simp, norm_cast]
theorem quaternion_algebra.nat_cast_im_k {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (n : ) :
@[simp, norm_cast]
theorem quaternion_algebra.nat_cast_im {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (n : ) :
n.im = 0
@[norm_cast]
theorem quaternion_algebra.coe_nat_cast {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (n : ) :
@[simp, norm_cast]
theorem quaternion_algebra.int_cast_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (z : ) :
@[simp, norm_cast]
theorem quaternion_algebra.int_cast_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (z : ) :
@[simp, norm_cast]
theorem quaternion_algebra.int_cast_im_j {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (z : ) :
@[simp, norm_cast]
theorem quaternion_algebra.int_cast_im_k {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (z : ) :
@[simp, norm_cast]
theorem quaternion_algebra.int_cast_im {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (z : ) :
z.im = 0
@[norm_cast]
theorem quaternion_algebra.coe_int_cast {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (z : ) :
@[protected, instance]
def quaternion_algebra.ring {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
ring c₁ c₂)
Equations
@[simp, norm_cast]
theorem quaternion_algebra.coe_mul {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x y : R) :
(x * y) = x * y
@[protected, instance]
def quaternion_algebra.algebra {S : Type u_1} {R : Type u_3} [comm_ring R] {c₁ c₂ : R} [ R] :
c₁ c₂)
Equations
theorem quaternion_algebra.algebra_map_eq {R : Type u_3} [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_3} [comm_ring R] (c₁ c₂ : R) :
c₂ →ₗ[R] R
Equations
@[simp]
theorem quaternion_algebra.re_lm_apply {R : Type u_3} [comm_ring R] (c₁ c₂ : R) (self : c₂) :
c₂) self = self.re
def quaternion_algebra.im_i_lm {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
c₂ →ₗ[R] R
Equations
@[simp]
theorem quaternion_algebra.im_i_lm_apply {R : Type u_3} [comm_ring R] (c₁ c₂ : R) (self : c₂) :
c₂) self = self.im_i
@[simp]
theorem quaternion_algebra.im_j_lm_apply {R : Type u_3} [comm_ring R] (c₁ c₂ : R) (self : c₂) :
c₂) self = self.im_j
def quaternion_algebra.im_j_lm {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
c₂ →ₗ[R] R
Equations
@[simp]
theorem quaternion_algebra.im_k_lm_apply {R : Type u_3} [comm_ring R] (c₁ c₂ : R) (self : c₂) :
c₂) self = self.im_k
def quaternion_algebra.im_k_lm {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
c₂ →ₗ[R] R
Equations
def quaternion_algebra.linear_equiv_tuple {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
c₂ ≃ₗ[R] fin 4 R

quaternion_algebra.equiv_tuple as a linear equivalence.

Equations
@[simp]
theorem quaternion_algebra.coe_linear_equiv_tuple {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
@[simp]
theorem quaternion_algebra.coe_linear_equiv_tuple_symm {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
.symm) = c₂).symm)
noncomputable def quaternion_algebra.basis_one_i_j_k {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
basis (fin 4) R c₁ c₂)

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

Equations
@[simp]
theorem quaternion_algebra.coe_basis_one_i_j_k_repr {R : Type u_3} [comm_ring R] (c₁ c₂ : R) (q : c₂) :
(.repr) q) = ![q.re, q.im_i, q.im_j, q.im_k]
@[protected, instance]
def quaternion_algebra.module.finite {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
c₁ c₂)
@[protected, instance]
def quaternion_algebra.module.free {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
c₁ c₂)
theorem quaternion_algebra.rank_eq_four {R : Type u_3} [comm_ring R] (c₁ c₂ : R)  :
c₁ c₂) = 4
theorem quaternion_algebra.finrank_eq_four {R : Type u_3} [comm_ring R] (c₁ c₂ : R)  :
c₁ c₂) = 4
@[simp, norm_cast]
theorem quaternion_algebra.coe_sub {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x y : R) :
(x - y) = x - y
@[simp, norm_cast]
theorem quaternion_algebra.coe_pow {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) (n : ) :
(x ^ n) = x ^ n
theorem quaternion_algebra.coe_commutes {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (r : R) (a : c₂) :
r * a = a * r
theorem quaternion_algebra.coe_commute {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (r : R) (a : c₂) :
a
theorem quaternion_algebra.coe_mul_eq_smul {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (r : R) (a : c₂) :
r * a = r a
theorem quaternion_algebra.mul_coe_eq_smul {R : Type u_3} [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_3} [comm_ring R] {c₁ c₂ : R} :
c₁ c₂)) = coe
theorem quaternion_algebra.smul_coe {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x y : R) :
x y = (x * y)
@[protected, instance]
def quaternion_algebra.has_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
has_star c₁ c₂)

Quaternion conjugate.

Equations
@[simp]
theorem quaternion_algebra.re_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
.re = a.re
@[simp]
theorem quaternion_algebra.im_i_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
@[simp]
theorem quaternion_algebra.im_j_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
@[simp]
theorem quaternion_algebra.im_k_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
@[simp]
theorem quaternion_algebra.im_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
.im = -a.im
@[simp]
theorem quaternion_algebra.star_mk {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a₁ a₂ a₃ a₄ : R) :
has_star.star {re := a₁, im_i := a₂, im_j := a₃, im_k := a₄} = {re := a₁, im_i := -a₂, im_j := -a₃, im_k := -a₄}
@[protected, instance]
def quaternion_algebra.star_ring {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
star_ring c₁ c₂)
Equations
theorem quaternion_algebra.self_add_star' {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= (2 * a.re)
theorem quaternion_algebra.self_add_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= 2 * (a.re)
theorem quaternion_algebra.star_add_self' {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= (2 * a.re)
theorem quaternion_algebra.star_add_self {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= 2 * (a.re)
theorem quaternion_algebra.star_eq_two_re_sub {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= (2 * a.re) - a
@[protected, instance]
def quaternion_algebra.is_star_normal {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
@[simp, norm_cast]
theorem quaternion_algebra.star_coe {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
@[simp]
theorem quaternion_algebra.star_im {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= -a.im
@[simp]
theorem quaternion_algebra.star_smul {S : Type u_1} {R : Type u_3} [comm_ring R] {c₁ c₂ : R} [monoid S] [ R] (s : S) (a : c₂) :
theorem quaternion_algebra.eq_re_of_eq_coe {R : Type u_3} [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_3} [comm_ring R] {c₁ c₂ : R} {a : c₂} :
a = (a.re)
@[simp]
theorem quaternion_algebra.star_eq_self {R : Type u_3} [comm_ring R] [char_zero R] {c₁ c₂ : R} {a : c₂} :
a = (a.re)
theorem quaternion_algebra.star_eq_neg {R : Type u_3} [comm_ring R] [char_zero R] {c₁ c₂ : R} {a : c₂} :
a.re = 0
theorem quaternion_algebra.star_mul_eq_coe {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= * a).re)
theorem quaternion_algebra.mul_star_eq_coe {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : c₂) :
= ((a * .re)
def quaternion_algebra.star_ae {R : Type u_3} [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_star_ae {R : Type u_3} [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
@[simp]
theorem quaternion.equiv_prod_symm_apply_im_k (R : Type u_1) [has_one R] [has_neg R] (a : R × R × R × R) :
@[simp]
theorem quaternion.equiv_prod_apply (R : Type u_1) [has_one R] [has_neg R] (a : (-1) (-1)) :
= (a.re, a.im_i, a.im_j, a.im_k)
@[simp]
theorem quaternion.equiv_prod_symm_apply_re (R : Type u_1) [has_one R] [has_neg R] (a : R × R × R × R) :
(.symm) a).re = a.fst
@[simp]
theorem quaternion.equiv_prod_symm_apply_im_j (R : Type u_1) [has_one R] [has_neg R] (a : R × R × R × R) :
@[simp]
theorem quaternion.equiv_prod_symm_apply_im_i (R : Type u_1) [has_one R] [has_neg R] (a : R × R × R × R) :
(.symm) a).im_i = a.snd.fst
@[simp]
theorem quaternion.equiv_tuple_symm_apply (R : Type u_1) [has_one R] [has_neg R] (a : fin 4 R) :
.symm) a = {re := a 0, im_i := a 1, im_j := a 2, im_k := a 3}
def quaternion.equiv_tuple (R : Type u_1) [has_one R] [has_neg R] :
(fin 4 R)

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

Equations
@[simp]
theorem quaternion.equiv_tuple_apply (R : Type u_1) [has_one R] [has_neg R] (x : quaternion R) :
= ![x.re, x.im_i, x.im_j, x.im_k]
@[protected, instance]
def quaternion.has_coe_t {R : Type u_3} [comm_ring R] :
Equations
@[protected, instance]
def quaternion.ring {R : Type u_3} [comm_ring R] :
Equations
@[protected, instance]
def quaternion.inhabited {R : Type u_3} [comm_ring R] :
Equations
@[protected, instance]
def quaternion.has_smul {S : Type u_1} {R : Type u_3} [comm_ring R] [ R] :
Equations
@[protected, instance]
def quaternion.is_scalar_tower {S : Type u_1} {T : Type u_2} {R : Type u_3} [comm_ring R] [ T] [ R] [ R] [ R] :
@[protected, instance]
def quaternion.smul_comm_class {S : Type u_1} {T : Type u_2} {R : Type u_3} [comm_ring R] [ R] [ R] [ R] :
@[protected, instance]
def quaternion.algebra {S : Type u_1} {R : Type u_3} [comm_ring R] [ R] :
Equations
@[protected, instance]
def quaternion.star_ring {R : Type u_3} [comm_ring R] :
Equations
@[ext]
theorem quaternion.ext {R : Type u_3} [comm_ring R] (a b : quaternion R) :
a.re = b.re a.im_i = b.im_i a.im_j = b.im_j a.im_k = b.im_k a = b
theorem quaternion.ext_iff {R : Type u_3} [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
def quaternion.im {R : Type u_3} [comm_ring R] (x : quaternion R) :

The imaginary part of a quaternion.

Equations
@[simp]
theorem quaternion.im_re {R : Type u_3} [comm_ring R] (a : quaternion R) :
a.im.re = 0
@[simp]
theorem quaternion.im_im_i {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.im_im_j {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.im_im_k {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.im_idem {R : Type u_3} [comm_ring R] (a : quaternion R) :
a.im.im = a.im
@[simp]
theorem quaternion.re_add_im {R : Type u_3} [comm_ring R] (a : quaternion R) :
(a.re) + a.im = a
@[simp]
theorem quaternion.sub_self_im {R : Type u_3} [comm_ring R] (a : quaternion R) :
a - a.im = (a.re)
@[simp]
theorem quaternion.sub_self_re {R : Type u_3} [comm_ring R] (a : quaternion R) :
a - (a.re) = a.im
@[simp, norm_cast]
theorem quaternion.coe_re {R : Type u_3} [comm_ring R] (x : R) :
x.re = x
@[simp, norm_cast]
theorem quaternion.coe_im_i {R : Type u_3} [comm_ring R] (x : R) :
@[simp, norm_cast]
theorem quaternion.coe_im_j {R : Type u_3} [comm_ring R] (x : R) :
@[simp, norm_cast]
theorem quaternion.coe_im_k {R : Type u_3} [comm_ring R] (x : R) :
@[simp, norm_cast]
theorem quaternion.coe_im {R : Type u_3} [comm_ring R] (x : R) :
x.im = 0
@[simp]
theorem quaternion.zero_re {R : Type u_3} [comm_ring R] :
0.re = 0
@[simp]
theorem quaternion.zero_im_i {R : Type u_3} [comm_ring R] :
0.im_i = 0
@[simp]
theorem quaternion.zero_im_j {R : Type u_3} [comm_ring R] :
0.im_j = 0
@[simp]
theorem quaternion.zero_im_k {R : Type u_3} [comm_ring R] :
0.im_k = 0
@[simp]
theorem quaternion.zero_im {R : Type u_3} [comm_ring R] :
0.im = 0
@[simp, norm_cast]
theorem quaternion.coe_zero {R : Type u_3} [comm_ring R] :
0 = 0
@[simp]
theorem quaternion.one_re {R : Type u_3} [comm_ring R] :
1.re = 1
@[simp]
theorem quaternion.one_im_i {R : Type u_3} [comm_ring R] :
1.im_i = 0
@[simp]
theorem quaternion.one_im_j {R : Type u_3} [comm_ring R] :
1.im_j = 0
@[simp]
theorem quaternion.one_im_k {R : Type u_3} [comm_ring R] :
1.im_k = 0
@[simp]
theorem quaternion.one_im {R : Type u_3} [comm_ring R] :
1.im = 0
@[simp, norm_cast]
theorem quaternion.coe_one {R : Type u_3} [comm_ring R] :
1 = 1
@[simp]
theorem quaternion.add_re {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a + b).re = a.re + b.re
@[simp]
theorem quaternion.add_im_i {R : Type u_3} [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_3} [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_3} [comm_ring R] (a b : quaternion R) :
(a + b).im_k = a.im_k + b.im_k
@[simp]
theorem quaternion.add_im {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a + b).im = a.im + b.im
@[simp, norm_cast]
theorem quaternion.coe_add {R : Type u_3} [comm_ring R] (x y : R) :
(x + y) = x + y
@[simp]
theorem quaternion.neg_re {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).re = -a.re
@[simp]
theorem quaternion.neg_im_i {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).im_i = -a.im_i
@[simp]
theorem quaternion.neg_im_j {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).im_j = -a.im_j
@[simp]
theorem quaternion.neg_im_k {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).im_k = -a.im_k
@[simp]
theorem quaternion.neg_im {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).im = -a.im
@[simp, norm_cast]
theorem quaternion.coe_neg {R : Type u_3} [comm_ring R] (x : R) :
@[simp]
theorem quaternion.sub_re {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a - b).re = a.re - b.re
@[simp]
theorem quaternion.sub_im_i {R : Type u_3} [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_3} [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_3} [comm_ring R] (a b : quaternion R) :
(a - b).im_k = a.im_k - b.im_k
@[simp]
theorem quaternion.sub_im {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a - b).im = a.im - b.im
@[simp, norm_cast]
theorem quaternion.coe_sub {R : Type u_3} [comm_ring R] (x y : R) :
(x - y) = x - y
@[simp]
theorem quaternion.mul_re {R : Type u_3} [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_3} [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_3} [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_3} [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_3} [comm_ring R] (x y : R) :
(x * y) = x * y
@[simp, norm_cast]
theorem quaternion.coe_pow {R : Type u_3} [comm_ring R] (x : R) (n : ) :
(x ^ n) = x ^ n
@[simp, norm_cast]
theorem quaternion.nat_cast_re {R : Type u_3} [comm_ring R] (n : ) :
@[simp, norm_cast]
theorem quaternion.nat_cast_im_i {R : Type u_3} [comm_ring R] (n : ) :
@[simp, norm_cast]
theorem quaternion.nat_cast_im_j {R : Type u_3} [comm_ring R] (n : ) :
@[simp, norm_cast]
theorem quaternion.nat_cast_im_k {R : Type u_3} [comm_ring R] (n : ) :
@[simp, norm_cast]
theorem quaternion.nat_cast_im {R : Type u_3} [comm_ring R] (n : ) :
n.im = 0
@[norm_cast]
theorem quaternion.coe_nat_cast {R : Type u_3} [comm_ring R] (n : ) :
@[simp, norm_cast]
theorem quaternion.int_cast_re {R : Type u_3} [comm_ring R] (z : ) :
@[simp, norm_cast]
theorem quaternion.int_cast_im_i {R : Type u_3} [comm_ring R] (z : ) :
@[simp, norm_cast]
theorem quaternion.int_cast_im_j {R : Type u_3} [comm_ring R] (z : ) :
@[simp, norm_cast]
theorem quaternion.int_cast_im_k {R : Type u_3} [comm_ring R] (z : ) :
@[simp, norm_cast]
theorem quaternion.int_cast_im {R : Type u_3} [comm_ring R] (z : ) :
z.im = 0
@[norm_cast]
theorem quaternion.coe_int_cast {R : Type u_3} [comm_ring R] (z : ) :
theorem quaternion.coe_injective {R : Type u_3} [comm_ring R] :
@[simp]
theorem quaternion.coe_inj {R : Type u_3} [comm_ring R] {x y : R} :
x = y x = y
@[simp]
theorem quaternion.smul_re {S : Type u_1} {R : Type u_3} [comm_ring R] (a : quaternion R) [ R] (s : S) :
(s a).re = s a.re
@[simp]
theorem quaternion.smul_im_i {S : Type u_1} {R : Type u_3} [comm_ring R] (a : quaternion R) [ R] (s : S) :
(s a).im_i = s a.im_i
@[simp]
theorem quaternion.smul_im_j {S : Type u_1} {R : Type u_3} [comm_ring R] (a : quaternion R) [ R] (s : S) :
(s a).im_j = s a.im_j
@[simp]
theorem quaternion.smul_im_k {S : Type u_1} {R : Type u_3} [comm_ring R] (a : quaternion R) [ R] (s : S) :
(s a).im_k = s a.im_k
@[simp]
theorem quaternion.smul_im {S : Type u_1} {R : Type u_3} [comm_ring R] (a : quaternion R) [ R] (s : S) :
(s a).im = s a.im
@[simp, norm_cast]
theorem quaternion.coe_smul {S : Type u_1} {R : Type u_3} [comm_ring R] [ R] (s : S) (r : R) :
(s r) = s r
theorem quaternion.coe_commutes {R : Type u_3} [comm_ring R] (r : R) (a : quaternion R) :
r * a = a * r
theorem quaternion.coe_commute {R : Type u_3} [comm_ring R] (r : R) (a : quaternion R) :
a
theorem quaternion.coe_mul_eq_smul {R : Type u_3} [comm_ring R] (r : R) (a : quaternion R) :
r * a = r a
theorem quaternion.mul_coe_eq_smul {R : Type u_3} [comm_ring R] (r : R) (a : quaternion R) :
a * r = r a
@[simp]
theorem quaternion.algebra_map_def {R : Type u_3} [comm_ring R] :
theorem quaternion.smul_coe {R : Type u_3} [comm_ring R] (x y : R) :
x y = (x * y)
@[protected, instance]
@[protected, instance]
def quaternion.module.free {R : Type u_3} [comm_ring R] :
theorem quaternion.rank_eq_four {R : Type u_3} [comm_ring R]  :
(quaternion R) = 4
theorem quaternion.finrank_eq_four {R : Type u_3} [comm_ring R]  :
@[simp]
theorem quaternion.star_re {R : Type u_3} [comm_ring R] (a : quaternion R) :
.re = a.re
@[simp]
theorem quaternion.star_im_i {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.star_im_j {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.star_im_k {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.star_im {R : Type u_3} [comm_ring R] (a : quaternion R) :
.im = -a.im
theorem quaternion.self_add_star' {R : Type u_3} [comm_ring R] (a : quaternion R) :
= (2 * a.re)
theorem quaternion.self_add_star {R : Type u_3} [comm_ring R] (a : quaternion R) :
= 2 * (a.re)
theorem quaternion.star_add_self' {R : Type u_3} [comm_ring R] (a : quaternion R) :
= (2 * a.re)
theorem quaternion.star_add_self {R : Type u_3} [comm_ring R] (a : quaternion R) :
= 2 * (a.re)
theorem quaternion.star_eq_two_re_sub {R : Type u_3} [comm_ring R] (a : quaternion R) :
= (2 * a.re) - a
@[simp, norm_cast]
theorem quaternion.star_coe {R : Type u_3} [comm_ring R] (x : R) :
@[simp]
theorem quaternion.im_star {R : Type u_3} [comm_ring R] (a : quaternion R) :
= -a.im
@[simp]
theorem quaternion.star_smul {S : Type u_1} {R : Type u_3} [comm_ring R] [monoid S] [ R] (s : S) (a : quaternion R) :
theorem quaternion.eq_re_of_eq_coe {R : Type u_3} [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_3} [comm_ring R] {a : quaternion R} :
a = (a.re)
@[simp]
theorem quaternion.star_eq_self {R : Type u_3} [comm_ring R] [char_zero R] {a : quaternion R} :
a = (a.re)
@[simp]
theorem quaternion.star_eq_neg {R : Type u_3} [comm_ring R] [char_zero R] {a : quaternion R} :
a.re = 0
theorem quaternion.star_mul_eq_coe {R : Type u_3} [comm_ring R] (a : quaternion R) :
= * a).re)
theorem quaternion.mul_star_eq_coe {R : Type u_3} [comm_ring R] (a : quaternion R) :
= ((a * .re)

Quaternion conjugate as an alg_equiv to the opposite ring.

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

Square of the norm.

Equations
theorem quaternion.norm_sq_def {R : Type u_3} [comm_ring R] (a : quaternion R) :
= (a * .re
theorem quaternion.norm_sq_def' {R : Type u_3} [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_3} [comm_ring R] (x : R) :
= x ^ 2
@[simp]
theorem quaternion.norm_sq_star {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[norm_cast]
theorem quaternion.norm_sq_nat_cast {R : Type u_3} [comm_ring R] (n : ) :
= n ^ 2
@[norm_cast]
theorem quaternion.norm_sq_int_cast {R : Type u_3} [comm_ring R] (z : ) :
= z ^ 2
@[simp]
theorem quaternion.norm_sq_neg {R : Type u_3} [comm_ring R] (a : quaternion R) :
theorem quaternion.self_mul_star {R : Type u_3} [comm_ring R] (a : quaternion R) :
=
theorem quaternion.star_mul_self {R : Type u_3} [comm_ring R] (a : quaternion R) :
=
theorem quaternion.im_sq {R : Type u_3} [comm_ring R] (a : quaternion R) :
a.im ^ 2 =
theorem quaternion.norm_sq_smul {R : Type u_3} [comm_ring R] (r : R) (q : quaternion R) :
theorem quaternion.norm_sq_add {R : Type u_3} [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.no_zero_divisors {R : Type u_1}  :
@[protected, instance]
def quaternion.is_domain {R : Type u_1}  :
theorem quaternion.sq_eq_norm_sq {R : Type u_1} {a : quaternion R} :
a ^ 2 = a = (a.re)
theorem quaternion.sq_eq_neg_norm_sq {R : Type u_1} {a : quaternion R} :
a ^ 2 = a.re = 0
@[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.group_with_zero {R : Type u_1}  :
Equations
@[simp, norm_cast]
theorem quaternion.coe_inv {R : Type u_1} (x : R) :
@[simp, norm_cast]
theorem quaternion.coe_div {R : Type u_1} (x y : R) :
(x / y) = x / y
@[simp, norm_cast]
theorem quaternion.coe_zpow {R : Type u_1} (x : R) (z : ) :
(x ^ z) = x ^ z
@[protected, instance]
def quaternion.division_ring {R : Type u_1}  :
Equations
@[simp, norm_cast]
theorem quaternion.rat_cast_re {R : Type u_1} (q : ) :
@[simp, norm_cast]
theorem quaternion.rat_cast_im_i {R : Type u_1} (q : ) :
@[simp, norm_cast]
theorem quaternion.rat_cast_im_j {R : Type u_1} (q : ) :
@[simp, norm_cast]
theorem quaternion.rat_cast_im_k {R : Type u_1} (q : ) :
@[simp, norm_cast]
theorem quaternion.rat_cast_im {R : Type u_1} (q : ) :
q.im = 0
@[norm_cast]
theorem quaternion.coe_rat_cast {R : Type u_1} (q : ) :
@[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) :
@[simp]
theorem quaternion.norm_sq_zpow {R : Type u_1} (a : quaternion R) (z : ) :
@[norm_cast]
theorem quaternion.norm_sq_rat_cast {R : Type u_1} (q : ) :
= q ^ 2
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]
@[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]