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

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
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
@[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) :
@[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)
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_im_i {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_im_j {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
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
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_im_k {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
@[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
@[protected, instance]
def quaternion_algebra.has_coe_t {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
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} :
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} :
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} :
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 : quaternion_algebra R c₁ 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 : quaternion_algebra R c₁ 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 : quaternion_algebra R c₁ 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 : quaternion_algebra R c₁ 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} :
Equations
@[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
@[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
@[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
@[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
@[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 : quaternion_algebra R c₁ 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 : quaternion_algebra R c₁ 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} :
Equations
@[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
@[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
@[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 : 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
@[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
@[protected, instance]
def quaternion_algebra.has_mul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :

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 : 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
@[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
@[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.algebra {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
algebra R (quaternion_algebra R c₁ c₂)
Equations
@[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
@[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
@[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
@[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
@[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) :
(algebra_map R (quaternion_algebra 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) :

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 : quaternion_algebra R c₁ c₂) :
(quaternion_algebra.re_lm R c₁ c₂) self = self.re
@[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
@[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
@[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
@[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 : quaternion_algebra R c₁ c₂) :
r * a = a * r
theorem quaternion_algebra.coe_commute {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) :
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
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
@[simp, norm_cast]
theorem quaternion_algebra.coe_algebra_map {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
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} :

Quaternion conjugate.

Equations
@[simp]
theorem quaternion_algebra.re_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem quaternion_algebra.im_i_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem quaternion_algebra.im_j_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem quaternion_algebra.im_k_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ 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.self_add_conj' {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
theorem quaternion_algebra.self_add_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
theorem quaternion_algebra.conj_add_self' {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
theorem quaternion_algebra.conj_add_self {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
theorem quaternion_algebra.conj_eq_two_re_sub {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
theorem quaternion_algebra.commute_conj_self {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
theorem quaternion_algebra.commute_self_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
@[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 : quaternion_algebra R c₁ 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 : quaternion_algebra R c₁ 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 : quaternion_algebra R c₁ c₂} :
@[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₂} :
theorem quaternion_algebra.conj_zero {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
@[simp]
theorem quaternion_algebra.star_def {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
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
@[protected, instance]
def quaternion.ring {R : Type u_1} [comm_ring R] :
Equations
@[protected, instance]
def quaternion.algebra {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.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_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
@[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) :
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.smul_coe {R : Type u_1} [comm_ring R] (x y : R) :
x y = (x * y)

Quaternion conjugate.

Equations
@[simp]
theorem quaternion.conj_re {R : Type u_1} [comm_ring R] (a : quaternion R) :
@[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) :
theorem quaternion.self_add_conj' {R : Type u_1} [comm_ring R] (a : quaternion R) :
theorem quaternion.self_add_conj {R : Type u_1} [comm_ring R] (a : quaternion R) :
theorem quaternion.conj_add_self' {R : Type u_1} [comm_ring R] (a : quaternion R) :
theorem quaternion.conj_add_self {R : Type u_1} [comm_ring R] (a : quaternion R) :
@[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)
@[simp]
@[simp]
theorem quaternion.conj_zero {R : Type u_1} [comm_ring R] :

Quaternion conjugate as an alg_equiv to the opposite ring.

Equations

Square of the norm.

Equations
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
theorem quaternion.norm_sq_coe {R : Type u_1} [comm_ring R] (x : R) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
theorem cardinal.mk_quaternion_algebra {R : Type u_1} (c₁ c₂ : R) :

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

The cardinality of a quaternion algebra, as a set.

@[simp]

The cardinality of the quaternions, as a type.

@[simp]

The cardinality of the quaternions, as a set.