mathlib documentation

data.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 : ℍ[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
@[protected, instance]
def quaternion_algebra.has_coe_t {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
has_coe_t 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
@[protected, 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, 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} :
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, 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 : ℍ[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
@[protected, instance]
def quaternion_algebra.has_add {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
has_add ℍ[R,c₁,c₂]
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₄}
@[protected, 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
@[protected, 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
@[protected, 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₁}
@[protected, instance]
def quaternion_algebra.algebra {R : Type u_1} [comm_ring R] {c₁ c₂ : R} :
algebra 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, norm_cast]
theorem quaternion_algebra.coe_add {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x y : R) :
(x + y) = x + y
@[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_neg {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (x : R) :
@[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 : ℍ[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₂]) :
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, 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} :
ℍ[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₂]) :
@[simp]
theorem quaternion_algebra.conj_mul {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₂]) :
theorem quaternion_algebra.self_add_conj {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
theorem quaternion_algebra.conj_add_self' {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
theorem quaternion_algebra.conj_add_self {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
theorem quaternion_algebra.conj_eq_two_re_sub {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
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 : commute a 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₂]} :
@[simp]
theorem quaternion_algebra.conj_fixed {R : Type u_1} [comm_ring R] [no_zero_divisors R] [char_zero R] {c₁ c₂ : R} {a : ℍ[R,c₁,c₂]} :
theorem quaternion_algebra.conj_mul_eq_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
theorem quaternion_algebra.mul_conj_eq_coe {R : Type u_1} [comm_ring R] {c₁ c₂ : R} (a : ℍ[R,c₁,c₂]) :
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₂]) :
@[protected, 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
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
@[protected, instance]
def quaternion.has_coe_t {R : Type u_1} [comm_ring R] :
Equations
@[protected, instance]
def quaternion.ring {R : Type u_1} [comm_ring R] :
Equations
@[protected, instance]
def quaternion.inhabited {R : Type u_1} [comm_ring R] :
Equations
@[protected, instance]
def quaternion.algebra {R : Type u_1} [comm_ring R] :
Equations
@[protected, instance]
def quaternion.star_ring {R : Type u_1} [comm_ring R] :
Equations
@[ext]
theorem quaternion.ext {R : Type u_1} [comm_ring R] (a b : ℍ[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, 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 : ℍ[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, 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 : ℍ[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, 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 : ℍ[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, 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 : ℍ[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, 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 : ℍ[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]) :
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]) :
@[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]
@[simp]
theorem quaternion.conj_mul {R : Type u_1} [comm_ring R] (a b : ℍ[R]) :
theorem quaternion.self_add_conj' {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
theorem quaternion.self_add_conj {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
theorem quaternion.conj_add_self' {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
theorem quaternion.conj_add_self {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
theorem quaternion.conj_eq_two_re_sub {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
theorem quaternion.commute_conj_self {R : Type u_1} [comm_ring R] (a : ℍ[R]) :
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 : commute a b) :
theorem commute.quaternion_conj {R : Type u_1} [comm_ring R] {a b : ℍ[R]} (h : commute a 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]} :
@[simp]
theorem quaternion.conj_fixed {R : Type u_1} [comm_ring R] [no_zero_divisors R] [char_zero R] {a : ℍ[R]} :
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]) :
@[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]

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 : ℍ[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) :
@[simp]
@[simp]
@[simp]
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations