data.quaternion

# Quaternions #

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

## Main definitions #

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

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

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

## Notation #

The following notation is available with open_locale quaternion.

• ℍ[R, c₁, c₂] : quaternion_algebra R c₁ c₂
• ℍ[R] : quaternions over R.

## Implementation notes #

We define quaternions over any ring R, not just ℝ to be able to deal with, e.g., integer or rational quaternions without using real numbers. In particular, all definitions in this file are computable.

## Tags #

quaternion

theorem quaternion_algebra.ext {R : Type u_1} {a b : R} (x y : ℍ[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 : ℍ[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.

@[simp]
theorem quaternion_algebra.mk.eta {R : Type u_1} {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
{re := a.re, im_i := a.im_i, im_j := a.im_j, im_k := a.im_k} = a
@[instance]
def quaternion_algebra.has_coe_t {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
ℍ[R,c₁,c₂]
Equations
@[simp]
theorem quaternion_algebra.coe_re {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
x.re = x
@[simp]
theorem quaternion_algebra.coe_im_i {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
@[simp]
theorem quaternion_algebra.coe_im_j {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
@[simp]
theorem quaternion_algebra.coe_im_k {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
theorem quaternion_algebra.coe_injective {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
@[simp]
theorem quaternion_algebra.coe_inj {R : Type u_1} [comm_ring R] {c₁ c₂ x y : R} :
x = y x = y
@[simp]
theorem quaternion_algebra.has_zero_zero_re {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
0.re = 0
@[simp]
theorem quaternion_algebra.has_zero_zero_im_i {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
0.im_i = 0
@[instance]
def quaternion_algebra.has_zero {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
has_zero ℍ[R,c₁,c₂]
Equations
@[simp]
theorem quaternion_algebra.has_zero_zero_im_k {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
0.im_k = 0
@[simp]
theorem quaternion_algebra.has_zero_zero_im_j {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
0.im_j = 0
@[simp]
theorem quaternion_algebra.coe_zero {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
0 = 0
@[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
@[instance]
def quaternion_algebra.has_one {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
has_one ℍ[R,c₁,c₂]
Equations
@[simp]
theorem quaternion_algebra.has_one_one_im_j {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
1.im_j = 0
@[simp]
theorem quaternion_algebra.has_one_one_im_k {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
1.im_k = 0
@[simp]
theorem quaternion_algebra.has_one_one_re {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
1.re = 1
@[simp]
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 : ℍ[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 : ℍ[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 : ℍ[R,c₁,c₂]) :
(a + b).im_j = a.im_j + b.im_j
@[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 : ℍ[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₄}
@[instance]
def quaternion_algebra.has_neg {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
has_neg ℍ[R,c₁,c₂]
Equations
@[simp]
theorem quaternion_algebra.has_neg_neg_im_i {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[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 : ℍ[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 : ℍ[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 : ℍ[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]
theorem quaternion_algebra.has_sub_sub_im_k {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : ℍ[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 : ℍ[R,c₁,c₂]) :
(a - b).im_j = a.im_j - b.im_j
@[instance]
def quaternion_algebra.has_sub {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
has_sub ℍ[R,c₁,c₂]
Equations
@[simp]
theorem quaternion_algebra.has_sub_sub_im_i {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : ℍ[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 : ℍ[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 : ℍ[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 : ℍ[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
@[instance]
def quaternion_algebra.has_mul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
has_mul ℍ[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
@[simp]
theorem quaternion_algebra.has_mul_mul_im_j {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : ℍ[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 : ℍ[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₁}
@[instance]
def quaternion_algebra.ring {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
ring ℍ[R,c₁,c₂]
Equations
@[instance]
def quaternion_algebra.algebra {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
ℍ[R,c₁,c₂]
Equations
@[simp]
theorem quaternion_algebra.smul_re {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : ℍ[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 : ℍ[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 : ℍ[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 : ℍ[R,c₁,c₂]) :
(r a).im_k = r a.im_k
@[simp]
theorem quaternion_algebra.coe_add {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x y : R) :
(x + y) = x + y
@[simp]
theorem quaternion_algebra.coe_sub {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x y : R) :
(x - y) = x - y
@[simp]
theorem quaternion_algebra.coe_neg {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
@[simp]
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 : ℍ[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 : ℍ[R,c₁,c₂]) :
a
theorem quaternion_algebra.coe_mul_eq_smul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : ℍ[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 : ℍ[R,c₁,c₂]) :
a * r = r a
@[simp]
theorem quaternion_algebra.coe_algebra_map {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
ℍ[R,c₁,c₂]) = coe
theorem quaternion_algebra.smul_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x y : R) :
x y = x * y
def quaternion_algebra.conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
ℍ[R,c₁,c₂] ≃ₗ[R] ℍ[R,c₁,c₂]

Quaternion conjugate.

Equations
@[simp]
theorem quaternion_algebra.re_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
@[simp]
theorem quaternion_algebra.im_i_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
@[simp]
theorem quaternion_algebra.im_j_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
@[simp]
theorem quaternion_algebra.im_k_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
@[simp]
theorem quaternion_algebra.conj_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
theorem quaternion_algebra.conj_add {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : ℍ[R,c₁,c₂]) :
@[simp]
theorem quaternion_algebra.conj_mul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : ℍ[R,c₁,c₂]) :
theorem quaternion_algebra.conj_conj_mul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : ℍ[R,c₁,c₂]) :
theorem quaternion_algebra.conj_mul_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : ℍ[R,c₁,c₂]) :
theorem quaternion_algebra.self_add_conj' {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
= 2 * a.re
theorem quaternion_algebra.self_add_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
= 2 * (a.re)
theorem quaternion_algebra.conj_add_self' {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
= 2 * a.re
theorem quaternion_algebra.conj_add_self {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
= 2 * (a.re)
theorem quaternion_algebra.conj_eq_two_re_sub {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
= 2 * a.re - a
theorem quaternion_algebra.commute_conj_self {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
theorem quaternion_algebra.commute_self_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
theorem quaternion_algebra.commute_conj_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} {a b : ℍ[R,c₁,c₂]} (h : b) :
@[simp]
theorem quaternion_algebra.conj_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
theorem quaternion_algebra.conj_smul {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (r : R) (a : ℍ[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 : ℍ[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 : ℍ[R,c₁,c₂]} :
a = (a.re)
@[simp]
theorem quaternion_algebra.conj_fixed {R : Type u_1} [comm_ring R] [char_zero R] {c₁ c₂ : R} {a : ℍ[R,c₁,c₂]} :
a = (a.re)
theorem quaternion_algebra.conj_mul_eq_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
= * a).re)
theorem quaternion_algebra.mul_conj_eq_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
= .re)
theorem quaternion_algebra.conj_zero {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
theorem quaternion_algebra.conj_neg {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
theorem quaternion_algebra.conj_sub {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a b : ℍ[R,c₁,c₂]) :
@[instance]
def quaternion_algebra.star_ring {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
Equations
@[simp]
theorem quaternion_algebra.star_def {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
def quaternion_algebra.conj_alg_equiv {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
ℍ[R,c₁,c₂] ≃ₐ[R] ℍ[R,c₁,c₂]ᵒᵖ

Quaternion conjugate as an alg_equiv to the opposite ring.

Equations
@[simp]
theorem quaternion_algebra.coe_conj_alg_equiv {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
def quaternion (R : Type u_1) [has_one R] [has_neg R] :
Type u_1

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

Equations
@[instance]
def quaternion.has_coe_t {R : Type u_1} [comm_ring R] :
Equations
@[instance]
def quaternion.ring {R : Type u_1} [comm_ring R] :
Equations
@[instance]
def quaternion.inhabited {R : Type u_1} [comm_ring R] :
Equations
@[instance]
def quaternion.algebra {R : Type u_1} [comm_ring R] :
Equations
@[instance]
def quaternion.star_ring {R : Type u_1} [comm_ring R] :
Equations
@[ext]
theorem quaternion.ext {R : Type u_1} [comm_ring R] (a b : ℍ[R]) :
a.re = b.rea.im_i = b.im_ia.im_j = b.im_ja.im_k = b.im_ka = b
theorem quaternion.ext_iff {R : Type u_1} [comm_ring R] {a b : ℍ[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]
theorem quaternion.coe_re {R : Type u_1} [comm_ring R] (x : R) :
x.re = x
@[simp]
theorem quaternion.coe_im_i {R : Type u_1} [comm_ring R] (x : R) :
@[simp]
theorem quaternion.coe_im_j {R : Type u_1} [comm_ring R] (x : R) :
@[simp]
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]
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]
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 : ℍ[R]) :
(a + b).re = a.re + b.re
@[simp]
theorem quaternion.add_im_i {R : Type u_1} [comm_ring R] (a b : ℍ[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 : ℍ[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 : ℍ[R]) :
(a + b).im_k = a.im_k + b.im_k
@[simp]
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 : ℍ[R]) :
(-a).re = -a.re
@[simp]
theorem quaternion.neg_im_i {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
(-a).im_i = -a.im_i
@[simp]
theorem quaternion.neg_im_j {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
(-a).im_j = -a.im_j
@[simp]
theorem quaternion.neg_im_k {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
(-a).im_k = -a.im_k
@[simp]
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 : ℍ[R]) :
(a - b).re = a.re - b.re
@[simp]
theorem quaternion.sub_im_i {R : Type u_1} [comm_ring R] (a b : ℍ[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 : ℍ[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 : ℍ[R]) :
(a - b).im_k = a.im_k - b.im_k
@[simp]
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 : ℍ[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 : ℍ[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 : ℍ[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 : ℍ[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]
theorem quaternion.coe_mul {R : Type u_1} [comm_ring R] (x y : R) :
x * y = (x) * y
theorem quaternion.coe_injective {R : Type u_1} [comm_ring R] :
@[simp]
theorem quaternion.coe_inj {R : Type u_1} [comm_ring R] {x y : R} :
x = y x = y
@[simp]
theorem quaternion.smul_re {R : Type u_1} [comm_ring R] (r : R) (a : ℍ[R]) :
(r a).re = r a.re
@[simp]
theorem quaternion.smul_im_i {R : Type u_1} [comm_ring R] (r : R) (a : ℍ[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 : ℍ[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 : ℍ[R]) :
(r a).im_k = r a.im_k
theorem quaternion.coe_commutes {R : Type u_1} [comm_ring R] (r : R) (a : ℍ[R]) :
(r) * a = a * r
theorem quaternion.coe_commute {R : Type u_1} [comm_ring R] (r : R) (a : ℍ[R]) :
a
theorem quaternion.coe_mul_eq_smul {R : Type u_1} [comm_ring R] (r : R) (a : ℍ[R]) :
(r) * a = r a
theorem quaternion.mul_coe_eq_smul {R : Type u_1} [comm_ring R] (r : R) (a : ℍ[R]) :
a * r = r a
@[simp]
theorem quaternion.algebra_map_def {R : Type u_1} [comm_ring R] :
theorem quaternion.smul_coe {R : Type u_1} [comm_ring R] (x y : R) :
x y = x * y
def quaternion.conj {R : Type u_1} [comm_ring R] :

Quaternion conjugate.

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

Alias of commute_conj_conj.

@[simp]
theorem quaternion.conj_coe {R : Type u_1} [comm_ring R] (x : R) :
@[simp]
theorem quaternion.conj_smul {R : Type u_1} [comm_ring R] (r : R) (a : ℍ[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 : ℍ[R]} {x : R} (h : a = x) :
a = (a.re)
theorem quaternion.eq_re_iff_mem_range_coe {R : Type u_1} [comm_ring R] {a : ℍ[R]} :
a = (a.re)
@[simp]
theorem quaternion.conj_fixed {R : Type u_1} [comm_ring R] [char_zero R] {a : ℍ[R]} :
a = (a.re)
theorem quaternion.conj_mul_eq_coe {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
theorem quaternion.mul_conj_eq_coe {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
= ((a * .re)
@[simp]
theorem quaternion.conj_zero {R : Type u_1} [comm_ring R] :
@[simp]
theorem quaternion.conj_neg {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
@[simp]
theorem quaternion.conj_sub {R : Type u_1} [comm_ring R] (a b : ℍ[R]) :

Quaternion conjugate as an alg_equiv` to the opposite ring.

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

Square of the norm.

Equations
theorem quaternion.norm_sq_def {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
= (a * .re
theorem quaternion.norm_sq_def' {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
= a.re ^ 2 + a.im_i ^ 2 + a.im_j ^ 2 + a.im_k ^ 2
theorem quaternion.norm_sq_coe {R : Type u_1} [comm_ring R] (x : R) :
= x ^ 2
@[simp]
theorem quaternion.norm_sq_neg {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
theorem quaternion.self_mul_conj {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
theorem quaternion.conj_mul_self {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
* a =
theorem quaternion.coe_norm_sq_add {R : Type u_1} [comm_ring R] (a b : ℍ[R]) :
@[simp]
theorem quaternion.norm_sq_eq_zero {R : Type u_1} {a : ℍ[R]} :
a = 0
theorem quaternion.norm_sq_ne_zero {R : Type u_1} {a : ℍ[R]} :
a 0
@[simp]
theorem quaternion.norm_sq_nonneg {R : Type u_1} {a : ℍ[R]} :
@[simp]
theorem quaternion.norm_sq_le_zero {R : Type u_1} {a : ℍ[R]} :
a = 0
@[instance]
def quaternion.domain {R : Type u_1}  :
Equations
@[instance]
def quaternion.has_inv {R : Type u_1}  :
Equations
theorem quaternion.has_inv_inv {R : Type u_1} (a : ℍ[R]) :
@[instance]
def quaternion.division_ring {R : Type u_1}  :
Equations
@[simp]
theorem quaternion.norm_sq_inv {R : Type u_1} (a : ℍ[R]) :
@[simp]
theorem quaternion.norm_sq_div {R : Type u_1} (a b : ℍ[R]) :