mathlib documentation

algebra.quaternion

Quaternions #

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]:

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

source
theorem quaternion_algebra.ext {R : Type u_1} {a b : R} (x y : quaternion_algebra R a 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
source
theorem quaternion_algebra.ext_iff {R : Type u_1} {a b : R} (x y : quaternion_algebra R a 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
source
@[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
source
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_re {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
(⇑((quaternion_algebra.equiv_prod c₁ c₂).symm) a).re = a.fst
source
@[simp]
theorem quaternion_algebra.equiv_prod_apply {R : Type u_1} (c₁ c₂ : R) (a : quaternion_algebra R c₁ c₂) :
⇑(quaternion_algebra.equiv_prod c₁ c₂) a = (a.re, a.im_i, a.im_j, a.im_k)
source
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_im_i {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
(⇑((quaternion_algebra.equiv_prod c₁ c₂).symm) a).im_i = a.snd.fst
source
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_im_j {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
(⇑((quaternion_algebra.equiv_prod c₁ c₂).symm) a).im_j = a.snd.snd.fst
source
def quaternion_algebra.equiv_prod {R : Type u_1} (c₁ c₂ : R) :
quaternion_algebra R c₁ c₂ ≃ R × R × R × R

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

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

quaternion_algebra.re as a linear_map

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

quaternion_algebra.im_i as a linear_map

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

quaternion_algebra.im_j as a linear_map

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

quaternion_algebra.im_k as a linear_map

Equations
source
@[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
source
@[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
source
theorem quaternion_algebra.coe_commutes {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) :
↑r * a = a * ↑r
source
theorem quaternion_algebra.coe_commute {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) :
commute ↑r a
source
theorem quaternion_algebra.coe_mul_eq_smul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) :
↑r * a = r • a
source
theorem quaternion_algebra.mul_coe_eq_smul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) :
a * ↑r = r • a
source
@[simp, norm_cast]
theorem quaternion_algebra.coe_algebra_map {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
⇑(algebra_map R (quaternion_algebra R c₁ c₂)) = coe
source
theorem quaternion_algebra.smul_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x y : R) :
x • ↑y = ↑(x * y)
source
def quaternion_algebra.conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
quaternion_algebra R c₁ c₂ ≃ₗ[R] quaternion_algebra R c₁ c₂

Quaternion conjugate.

Equations
source
@[simp]
theorem quaternion_algebra.re_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
(⇑quaternion_algebra.conj a).re = a.re
source
@[simp]
theorem quaternion_algebra.im_i_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
(⇑quaternion_algebra.conj a).im_i = -a.im_i
source
@[simp]
theorem quaternion_algebra.im_j_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
(⇑quaternion_algebra.conj a).im_j = -a.im_j
source
@[simp]
theorem quaternion_algebra.im_k_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
(⇑quaternion_algebra.conj a).im_k = -a.im_k
source
@[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₄}
source
@[simp]
theorem quaternion_algebra.conj_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
⇑quaternion_algebra.conj (⇑quaternion_algebra.conj a) = a
source
theorem quaternion_algebra.conj_add {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : quaternion_algebra R c₁ c₂) :
⇑quaternion_algebra.conj (a + b) = ⇑quaternion_algebra.conj a + ⇑quaternion_algebra.conj b
source
@[simp]
theorem quaternion_algebra.conj_mul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : quaternion_algebra R c₁ c₂) :
⇑quaternion_algebra.conj (a * b) = ⇑quaternion_algebra.conj b * ⇑quaternion_algebra.conj a
source
theorem quaternion_algebra.conj_conj_mul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : quaternion_algebra R c₁ c₂) :
⇑quaternion_algebra.conj (⇑quaternion_algebra.conj a * b) = ⇑quaternion_algebra.conj b * a
source
theorem quaternion_algebra.conj_mul_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : quaternion_algebra R c₁ c₂) :
⇑quaternion_algebra.conj (a * ⇑quaternion_algebra.conj b) = b * ⇑quaternion_algebra.conj a
source
theorem quaternion_algebra.self_add_conj' {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
a + ⇑quaternion_algebra.conj a = ↑(2 * a.re)
source
theorem quaternion_algebra.self_add_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
a + ⇑quaternion_algebra.conj a = 2 * ↑(a.re)
source
theorem quaternion_algebra.conj_add_self' {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
⇑quaternion_algebra.conj a + a = ↑(2 * a.re)
source
theorem quaternion_algebra.conj_add_self {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
⇑quaternion_algebra.conj a + a = 2 * ↑(a.re)
source
theorem quaternion_algebra.conj_eq_two_re_sub {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
⇑quaternion_algebra.conj a = ↑(2 * a.re) - a
source
theorem quaternion_algebra.commute_conj_self {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
commute (⇑quaternion_algebra.conj a) a
source
theorem quaternion_algebra.commute_self_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
commute a (⇑quaternion_algebra.conj a)
source
theorem quaternion_algebra.commute_conj_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} {a b : quaternion_algebra R c₁ c₂} (h : commute a b) :
commute (⇑quaternion_algebra.conj a) (⇑quaternion_algebra.conj b)
source
@[simp]
theorem quaternion_algebra.conj_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
⇑quaternion_algebra.conj ↑x = ↑x
source
theorem quaternion_algebra.conj_smul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) :
⇑quaternion_algebra.conj (r • a) = r • ⇑quaternion_algebra.conj a
source
@[simp]
theorem quaternion_algebra.conj_one {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
⇑quaternion_algebra.conj 1 = 1
source
theorem quaternion_algebra.eq_re_of_eq_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} {a : quaternion_algebra R c₁ c₂} {x : R} (h : a = ↑x) :
a = ↑(a.re)
source
theorem quaternion_algebra.eq_re_iff_mem_range_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} {a : quaternion_algebra R c₁ c₂} :
a = ↑(a.re) ↔ a ∈ set.range coe
source
@[simp]
theorem quaternion_algebra.conj_fixed {R : Type u_1} [comm_ring R] [no_zero_divisors R] [char_zero R] {c₁ c₂ : R} {a : quaternion_algebra R c₁ c₂} :
⇑quaternion_algebra.conj a = a ↔ a = ↑(a.re)
source
theorem quaternion_algebra.conj_mul_eq_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
⇑quaternion_algebra.conj a * a = ↑((⇑quaternion_algebra.conj a * a).re)
source
theorem quaternion_algebra.mul_conj_eq_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
a * ⇑quaternion_algebra.conj a = ↑((a * ⇑quaternion_algebra.conj a).re)
source
theorem quaternion_algebra.conj_zero {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
⇑quaternion_algebra.conj 0 = 0
source
theorem quaternion_algebra.conj_neg {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
⇑quaternion_algebra.conj (-a) = -⇑quaternion_algebra.conj a
source
theorem quaternion_algebra.conj_sub {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : quaternion_algebra R c₁ c₂) :
⇑quaternion_algebra.conj (a - b) = ⇑quaternion_algebra.conj a - ⇑quaternion_algebra.conj b
source
@[protected, instance]
def quaternion_algebra.star_ring {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
star_ring (quaternion_algebra R c₁ c₂)
Equations
source
@[simp]
theorem quaternion_algebra.star_def {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
has_star.star a = ⇑quaternion_algebra.conj a
source
def quaternion_algebra.conj_ae {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
quaternion_algebra R c₁ c₂ ≃ₐ[R] (quaternion_algebra R c₁ c₂)ᵐᵒᵖ

Quaternion conjugate as an alg_equiv to the opposite ring.

Equations
source
@[simp]
theorem quaternion_algebra.coe_conj_ae {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
⇑quaternion_algebra.conj_ae = mul_opposite.op ∘ ⇑quaternion_algebra.conj
source
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
Instances for quaternion
source
def quaternion.equiv_prod (R : Type u_1) [has_one R] [has_neg R] :
quaternion R ≃ R × R × R × R

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

Equations
source
@[protected, instance]
def quaternion.has_coe_t {R : Type u_1} [comm_ring R] :
has_coe_t R (quaternion R)
Equations
source
@[protected, instance]
def quaternion.ring {R : Type u_1} [comm_ring R] :
ring (quaternion R)
Equations
source
@[protected, instance]
def quaternion.inhabited {R : Type u_1} [comm_ring R] :
inhabited (quaternion R)
Equations
source
@[protected, instance]
def quaternion.algebra {R : Type u_1} [comm_ring R] :
algebra R (quaternion R)
Equations
source
@[protected, instance]
def quaternion.star_ring {R : Type u_1} [comm_ring R] :
star_ring (quaternion R)
Equations
source
@[ext]
theorem quaternion.ext {R : Type u_1} [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
source
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
source
@[simp, norm_cast]
theorem quaternion.coe_re {R : Type u_1} [comm_ring R] (x : R) :
↑x.re = x
source
@[simp, norm_cast]
theorem quaternion.coe_im_i {R : Type u_1} [comm_ring R] (x : R) :
↑x.im_i = 0
source
@[simp, norm_cast]
theorem quaternion.coe_im_j {R : Type u_1} [comm_ring R] (x : R) :
↑x.im_j = 0
source
@[simp, norm_cast]
theorem quaternion.coe_im_k {R : Type u_1} [comm_ring R] (x : R) :
↑x.im_k = 0
source
@[simp]
theorem quaternion.zero_re {R : Type u_1} [comm_ring R] :
0.re = 0
source
@[simp]
theorem quaternion.zero_im_i {R : Type u_1} [comm_ring R] :
0.im_i = 0
source
@[simp]
theorem quaternion.zero_im_j {R : Type u_1} [comm_ring R] :
0.im_j = 0
source
@[simp]
theorem quaternion.zero_im_k {R : Type u_1} [comm_ring R] :
0.im_k = 0
source
@[simp, norm_cast]
theorem quaternion.coe_zero {R : Type u_1} [comm_ring R] :
↑0 = 0
source
@[simp]
theorem quaternion.one_re {R : Type u_1} [comm_ring R] :
1.re = 1
source
@[simp]
theorem quaternion.one_im_i {R : Type u_1} [comm_ring R] :
1.im_i = 0
source
@[simp]
theorem quaternion.one_im_j {R : Type u_1} [comm_ring R] :
1.im_j = 0
source
@[simp]
theorem quaternion.one_im_k {R : Type u_1} [comm_ring R] :
1.im_k = 0
source
@[simp, norm_cast]
theorem quaternion.coe_one {R : Type u_1} [comm_ring R] :
↑1 = 1
source
@[simp]
theorem quaternion.add_re {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a + b).re = a.re + b.re
source
@[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
source
@[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
source
@[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
source
@[simp, norm_cast]
theorem quaternion.coe_add {R : Type u_1} [comm_ring R] (x y : R) :
↑(x + y) = ↑x + ↑y
source
@[simp]
theorem quaternion.neg_re {R : Type u_1} [comm_ring R] (a : quaternion R) :
(-a).re = -a.re
source
@[simp]
theorem quaternion.neg_im_i {R : Type u_1} [comm_ring R] (a : quaternion R) :
(-a).im_i = -a.im_i
source
@[simp]
theorem quaternion.neg_im_j {R : Type u_1} [comm_ring R] (a : quaternion R) :
(-a).im_j = -a.im_j
source
@[simp]
theorem quaternion.neg_im_k {R : Type u_1} [comm_ring R] (a : quaternion R) :
(-a).im_k = -a.im_k
source
@[simp, norm_cast]
theorem quaternion.coe_neg {R : Type u_1} [comm_ring R] (x : R) :
↑-x = -↑x
source
@[simp]
theorem quaternion.sub_re {R : Type u_1} [comm_ring R] (a b : quaternion R) :
(a - b).re = a.re - b.re
source
@[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
source
@[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
source
@[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
source
@[simp, norm_cast]
theorem quaternion.coe_sub {R : Type u_1} [comm_ring R] (x y : R) :
↑(x - y) = ↑x - ↑y
source
@[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
source
@[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
source
@[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
source
@[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
source
@[simp, norm_cast]
theorem quaternion.coe_mul {R : Type u_1} [comm_ring R] (x y : R) :
↑(x * y) = ↑x * ↑y
source
theorem quaternion.coe_injective {R : Type u_1} [comm_ring R] :
function.injective coe
source
@[simp]
theorem quaternion.coe_inj {R : Type u_1} [comm_ring R] {x y : R} :
↑x = ↑y ↔ x = y
source
@[simp]
theorem quaternion.smul_re {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
(r • a).re = r • a.re
source
@[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
source
@[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
source
@[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
source
theorem quaternion.coe_commutes {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
↑r * a = a * ↑r
source
theorem quaternion.coe_commute {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
commute ↑r a
source
theorem quaternion.coe_mul_eq_smul {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
↑r * a = r • a
source
theorem quaternion.mul_coe_eq_smul {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
a * ↑r = r • a
source
@[simp]
theorem quaternion.algebra_map_def {R : Type u_1} [comm_ring R] :
⇑(algebra_map R (quaternion R)) = coe
source
theorem quaternion.smul_coe {R : Type u_1} [comm_ring R] (x y : R) :
x • ↑y = ↑(x * y)
source
def quaternion.conj {R : Type u_1} [comm_ring R] :
quaternion R ≃ₗ[R] quaternion R

Quaternion conjugate.

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

Alias of quaternion.commute_conj_conj.

source
@[simp]
theorem quaternion.conj_coe {R : Type u_1} [comm_ring R] (x : R) :
⇑quaternion.conj ↑x = ↑x
source
@[simp]
theorem quaternion.conj_smul {R : Type u_1} [comm_ring R] (r : R) (a : quaternion R) :
⇑quaternion.conj (r • a) = r • ⇑quaternion.conj a
source
@[simp]
theorem quaternion.conj_one {R : Type u_1} [comm_ring R] :
⇑quaternion.conj 1 = 1
source
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)
source
theorem quaternion.eq_re_iff_mem_range_coe {R : Type u_1} [comm_ring R] {a : quaternion R} :
a = ↑(a.re) ↔ a ∈ set.range coe
source
@[simp]
theorem quaternion.conj_fixed {R : Type u_1} [comm_ring R] [no_zero_divisors R] [char_zero R] {a : quaternion R} :
⇑quaternion.conj a = a ↔ a = ↑(a.re)
source
theorem quaternion.conj_mul_eq_coe {R : Type u_1} [comm_ring R] (a : quaternion R) :
⇑quaternion.conj a * a = ↑((⇑quaternion.conj a * a).re)
source
theorem quaternion.mul_conj_eq_coe {R : Type u_1} [comm_ring R] (a : quaternion R) :
a * ⇑quaternion.conj a = ↑((a * ⇑quaternion.conj a).re)
source
@[simp]
theorem quaternion.conj_zero {R : Type u_1} [comm_ring R] :
⇑quaternion.conj 0 = 0
source
@[simp]
theorem quaternion.conj_neg {R : Type u_1} [comm_ring R] (a : quaternion R) :
⇑quaternion.conj (-a) = -⇑quaternion.conj a
source
@[simp]
theorem quaternion.conj_sub {R : Type u_1} [comm_ring R] (a b : quaternion R) :
⇑quaternion.conj (a - b) = ⇑quaternion.conj a - ⇑quaternion.conj b
source
def quaternion.conj_ae {R : Type u_1} [comm_ring R] :
quaternion R ≃ₐ[R] (quaternion R)ᵐᵒᵖ

Quaternion conjugate as an alg_equiv to the opposite ring.

Equations
source
@[simp]
theorem quaternion.coe_conj_ae {R : Type u_1} [comm_ring R] :
⇑quaternion.conj_ae = mul_opposite.op ∘ ⇑quaternion.conj
source
def quaternion.norm_sq {R : Type u_1} [comm_ring R] :
quaternion R →*₀ R

Square of the norm.

Equations
source
theorem quaternion.norm_sq_def {R : Type u_1} [comm_ring R] (a : quaternion R) :
⇑quaternion.norm_sq a = (a * ⇑quaternion.conj a).re
source
theorem quaternion.norm_sq_def' {R : Type u_1} [comm_ring R] (a : quaternion R) :
⇑quaternion.norm_sq a = a.re ^ 2 + a.im_i ^ 2 + a.im_j ^ 2 + a.im_k ^ 2
source
theorem quaternion.norm_sq_coe {R : Type u_1} [comm_ring R] (x : R) :
⇑quaternion.norm_sq ↑x = x ^ 2
source
@[simp]
theorem quaternion.norm_sq_neg {R : Type u_1} [comm_ring R] (a : quaternion R) :
⇑quaternion.norm_sq (-a) = ⇑quaternion.norm_sq a
source
theorem quaternion.self_mul_conj {R : Type u_1} [comm_ring R] (a : quaternion R) :
a * ⇑quaternion.conj a = ↑(⇑quaternion.norm_sq a)
source
theorem quaternion.conj_mul_self {R : Type u_1} [comm_ring R] (a : quaternion R) :
⇑quaternion.conj a * a = ↑(⇑quaternion.norm_sq a)
source
theorem quaternion.coe_norm_sq_add {R : Type u_1} [comm_ring R] (a b : quaternion R) :
↑(⇑quaternion.norm_sq (a + b)) = ↑(⇑quaternion.norm_sq a) + a * ⇑quaternion.conj b + b * ⇑quaternion.conj a + ↑(⇑quaternion.norm_sq b)
source
@[simp]
theorem quaternion.norm_sq_eq_zero {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} :
⇑quaternion.norm_sq a = 0 ↔ a = 0
source
theorem quaternion.norm_sq_ne_zero {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} :
⇑quaternion.norm_sq a ≠ 0 ↔ a ≠ 0
source
@[simp]
theorem quaternion.norm_sq_nonneg {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} :
0 ≤ ⇑quaternion.norm_sq a
source
@[simp]
theorem quaternion.norm_sq_le_zero {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} :
⇑quaternion.norm_sq a ≤ 0 ↔ a = 0
source
@[protected, instance]
def quaternion.nontrivial {R : Type u_1} [linear_ordered_comm_ring R] :
nontrivial (quaternion R)
source
@[protected, instance]
def quaternion.is_domain {R : Type u_1} [linear_ordered_comm_ring R] :
is_domain (quaternion R)
source
@[protected, instance]
def quaternion.has_inv {R : Type u_1} [linear_ordered_field R] :
has_inv (quaternion R)
Equations
source
theorem quaternion.has_inv_inv {R : Type u_1} [linear_ordered_field R] (a : quaternion R) :
a⁻¹ = (⇑quaternion.norm_sq a)⁻¹ • ⇑quaternion.conj a
source
@[protected, instance]
def quaternion.division_ring {R : Type u_1} [linear_ordered_field R] :
division_ring (quaternion R)
Equations
source
@[simp]
theorem quaternion.norm_sq_inv {R : Type u_1} [linear_ordered_field R] (a : quaternion R) :
⇑quaternion.norm_sq a⁻¹ = (⇑quaternion.norm_sq a)⁻¹
source
@[simp]
theorem quaternion.norm_sq_div {R : Type u_1} [linear_ordered_field R] (a b : quaternion R) :
⇑quaternion.norm_sq (a / b) = ⇑quaternion.norm_sq a / ⇑quaternion.norm_sq b
source
theorem cardinal.mk_quaternion_algebra {R : Type u_1} (c₁ c₂ : R) :
cardinal.mk (quaternion_algebra R c₁ c₂) = cardinal.mk R ^ 4

The cardinality of a quaternion algebra, as a type.

source
@[simp]
theorem cardinal.mk_quaternion_algebra_of_infinite {R : Type u_1} (c₁ c₂ : R) [infinite R] :
cardinal.mk (quaternion_algebra R c₁ c₂) = cardinal.mk R
source
theorem cardinal.mk_univ_quaternion_algebra {R : Type u_1} (c₁ c₂ : R) :
cardinal.mk ↥set.univ = cardinal.mk R ^ 4

The cardinality of a quaternion algebra, as a set.

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

The cardinality of the quaternions, as a type.

source
@[simp]
theorem cardinal.mk_quaternion_of_infinite (R : Type u_1) [has_one R] [has_neg R] [infinite R] :
cardinal.mk (quaternion R) = cardinal.mk R
source
@[simp]
theorem cardinal.mk_univ_quaternion (R : Type u_1) [has_one R] [has_neg R] :
cardinal.mk ↥set.univ = cardinal.mk R ^ 4

The cardinality of the quaternions, as a set.

source
@[simp]
theorem cardinal.mk_univ_quaternion_of_infinite (R : Type u_1) [has_one R] [has_neg R] [infinite R] :
cardinal.mk ↥set.univ = cardinal.mk R