mathlib3 documentation

algebra.quaternion

Quaternions #

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

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

Main definitions #

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

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

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

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

The imaginary part of a quaternion.

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

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

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

Quaternion conjugate.

Equations
@[simp]
theorem quaternion_algebra.re_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem quaternion_algebra.im_i_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem quaternion_algebra.im_j_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem quaternion_algebra.im_k_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem quaternion_algebra.im_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem quaternion_algebra.star_mk {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a₁ a₂ a₃ a₄ : R) :
has_star.star {re := a₁, im_i := a₂, im_j := a₃, im_k := a₄} = {re := a₁, im_i := -a₂, im_j := -a₃, im_k := -a₄}
theorem quaternion_algebra.self_add_star' {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
a + has_star.star a = (2 * a.re)
theorem quaternion_algebra.self_add_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
a + has_star.star a = 2 * (a.re)
theorem quaternion_algebra.star_add_self' {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
has_star.star a + a = (2 * a.re)
theorem quaternion_algebra.star_add_self {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
has_star.star a + a = 2 * (a.re)
theorem quaternion_algebra.star_eq_two_re_sub {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
has_star.star a = (2 * a.re) - a
@[protected, instance]
def quaternion_algebra.is_star_normal {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
@[simp, norm_cast]
theorem quaternion_algebra.star_coe {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
@[simp]
theorem quaternion_algebra.star_im {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem quaternion_algebra.star_smul {S : Type u_1} {R : Type u_3} [comm_ring R] {c₁ c₂ : R} [monoid S] [distrib_mul_action S R] (s : S) (a : quaternion_algebra R c₁ c₂) :
theorem quaternion_algebra.eq_re_of_eq_coe {R : Type u_3} [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_3} [comm_ring R] {c₁ c₂ : R} {a : quaternion_algebra R c₁ c₂} :
@[simp]
theorem quaternion_algebra.star_eq_self {R : Type u_3} [comm_ring R] [no_zero_divisors R] [char_zero R] {c₁ c₂ : R} {a : quaternion_algebra R c₁ c₂} :
theorem quaternion_algebra.star_eq_neg {R : Type u_3} [comm_ring R] [no_zero_divisors R] [char_zero R] {c₁ c₂ : R} {a : quaternion_algebra R c₁ c₂} :
theorem quaternion_algebra.star_mul_eq_coe {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
theorem quaternion_algebra.mul_star_eq_coe {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
def quaternion_algebra.star_ae {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :

Quaternion conjugate as an alg_equiv to the opposite ring.

Equations
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
@[simp]
theorem quaternion.equiv_prod_symm_apply_im_k (R : Type u_1) [has_one R] [has_neg R] (a : R × R × R × R) :
@[simp]
theorem quaternion.equiv_prod_apply (R : Type u_1) [has_one R] [has_neg R] (a : quaternion_algebra R (-1) (-1)) :
@[simp]
theorem quaternion.equiv_prod_symm_apply_re (R : Type u_1) [has_one R] [has_neg R] (a : R × R × R × R) :
@[simp]
theorem quaternion.equiv_prod_symm_apply_im_j (R : Type u_1) [has_one R] [has_neg R] (a : R × R × R × R) :
@[simp]
theorem quaternion.equiv_prod_symm_apply_im_i (R : Type u_1) [has_one R] [has_neg R] (a : R × R × R × R) :
@[simp]
theorem quaternion.equiv_tuple_symm_apply (R : Type u_1) [has_one R] [has_neg R] (a : fin 4 R) :
((quaternion.equiv_tuple R).symm) a = {re := a 0, im_i := a 1, im_j := a 2, im_k := a 3}
def quaternion.equiv_tuple (R : Type u_1) [has_one R] [has_neg R] :

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

Equations
@[simp]
theorem quaternion.equiv_tuple_apply (R : Type u_1) [has_one R] [has_neg R] (x : quaternion R) :
@[protected, instance]
def quaternion.ring {R : Type u_3} [comm_ring R] :
Equations
@[protected, instance]
def quaternion.has_smul {S : Type u_1} {R : Type u_3} [comm_ring R] [has_smul S R] :
Equations
@[protected, instance]
def quaternion.is_scalar_tower {S : Type u_1} {T : Type u_2} {R : Type u_3} [comm_ring R] [has_smul S T] [has_smul S R] [has_smul T R] [is_scalar_tower S T R] :
@[protected, instance]
def quaternion.smul_comm_class {S : Type u_1} {T : Type u_2} {R : Type u_3} [comm_ring R] [has_smul S R] [has_smul T R] [smul_comm_class S T R] :
@[protected, instance]
def quaternion.algebra {S : Type u_1} {R : Type u_3} [comm_ring R] [comm_semiring S] [algebra S R] :
Equations
@[ext]
theorem quaternion.ext {R : Type u_3} [comm_ring R] (a b : quaternion R) :
a.re = b.re a.im_i = b.im_i a.im_j = b.im_j a.im_k = b.im_k a = b
theorem quaternion.ext_iff {R : Type u_3} [comm_ring R] {a b : quaternion R} :
a = b a.re = b.re a.im_i = b.im_i a.im_j = b.im_j a.im_k = b.im_k
def quaternion.im {R : Type u_3} [comm_ring R] (x : quaternion R) :

The imaginary part of a quaternion.

Equations
@[simp]
theorem quaternion.im_re {R : Type u_3} [comm_ring R] (a : quaternion R) :
a.im.re = 0
@[simp]
theorem quaternion.im_im_i {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.im_im_j {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.im_im_k {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.im_idem {R : Type u_3} [comm_ring R] (a : quaternion R) :
a.im.im = a.im
@[simp]
theorem quaternion.re_add_im {R : Type u_3} [comm_ring R] (a : quaternion R) :
(a.re) + a.im = a
@[simp]
theorem quaternion.sub_self_im {R : Type u_3} [comm_ring R] (a : quaternion R) :
a - a.im = (a.re)
@[simp]
theorem quaternion.sub_self_re {R : Type u_3} [comm_ring R] (a : quaternion R) :
a - (a.re) = a.im
@[simp, norm_cast]
theorem quaternion.coe_re {R : Type u_3} [comm_ring R] (x : R) :
x.re = x
@[simp, norm_cast]
theorem quaternion.coe_im_i {R : Type u_3} [comm_ring R] (x : R) :
@[simp, norm_cast]
theorem quaternion.coe_im_j {R : Type u_3} [comm_ring R] (x : R) :
@[simp, norm_cast]
theorem quaternion.coe_im_k {R : Type u_3} [comm_ring R] (x : R) :
@[simp, norm_cast]
theorem quaternion.coe_im {R : Type u_3} [comm_ring R] (x : R) :
x.im = 0
@[simp]
theorem quaternion.zero_re {R : Type u_3} [comm_ring R] :
0.re = 0
@[simp]
theorem quaternion.zero_im_i {R : Type u_3} [comm_ring R] :
0.im_i = 0
@[simp]
theorem quaternion.zero_im_j {R : Type u_3} [comm_ring R] :
0.im_j = 0
@[simp]
theorem quaternion.zero_im_k {R : Type u_3} [comm_ring R] :
0.im_k = 0
@[simp]
theorem quaternion.zero_im {R : Type u_3} [comm_ring R] :
0.im = 0
@[simp, norm_cast]
theorem quaternion.coe_zero {R : Type u_3} [comm_ring R] :
0 = 0
@[simp]
theorem quaternion.one_re {R : Type u_3} [comm_ring R] :
1.re = 1
@[simp]
theorem quaternion.one_im_i {R : Type u_3} [comm_ring R] :
1.im_i = 0
@[simp]
theorem quaternion.one_im_j {R : Type u_3} [comm_ring R] :
1.im_j = 0
@[simp]
theorem quaternion.one_im_k {R : Type u_3} [comm_ring R] :
1.im_k = 0
@[simp]
theorem quaternion.one_im {R : Type u_3} [comm_ring R] :
1.im = 0
@[simp, norm_cast]
theorem quaternion.coe_one {R : Type u_3} [comm_ring R] :
1 = 1
@[simp]
theorem quaternion.add_re {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a + b).re = a.re + b.re
@[simp]
theorem quaternion.add_im_i {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a + b).im_i = a.im_i + b.im_i
@[simp]
theorem quaternion.add_im_j {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a + b).im_j = a.im_j + b.im_j
@[simp]
theorem quaternion.add_im_k {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a + b).im_k = a.im_k + b.im_k
@[simp]
theorem quaternion.add_im {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a + b).im = a.im + b.im
@[simp, norm_cast]
theorem quaternion.coe_add {R : Type u_3} [comm_ring R] (x y : R) :
(x + y) = x + y
@[simp]
theorem quaternion.neg_re {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).re = -a.re
@[simp]
theorem quaternion.neg_im_i {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).im_i = -a.im_i
@[simp]
theorem quaternion.neg_im_j {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).im_j = -a.im_j
@[simp]
theorem quaternion.neg_im_k {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).im_k = -a.im_k
@[simp]
theorem quaternion.neg_im {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).im = -a.im
@[simp, norm_cast]
theorem quaternion.coe_neg {R : Type u_3} [comm_ring R] (x : R) :
@[simp]
theorem quaternion.sub_re {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a - b).re = a.re - b.re
@[simp]
theorem quaternion.sub_im_i {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a - b).im_i = a.im_i - b.im_i
@[simp]
theorem quaternion.sub_im_j {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a - b).im_j = a.im_j - b.im_j
@[simp]
theorem quaternion.sub_im_k {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a - b).im_k = a.im_k - b.im_k
@[simp]
theorem quaternion.sub_im {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a - b).im = a.im - b.im
@[simp, norm_cast]
theorem quaternion.coe_sub {R : Type u_3} [comm_ring R] (x y : R) :
(x - y) = x - y
@[simp]
theorem quaternion.mul_re {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a * b).re = a.re * b.re - a.im_i * b.im_i - a.im_j * b.im_j - a.im_k * b.im_k
@[simp]
theorem quaternion.mul_im_i {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a * b).im_i = a.re * b.im_i + a.im_i * b.re + a.im_j * b.im_k - a.im_k * b.im_j
@[simp]
theorem quaternion.mul_im_j {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a * b).im_j = a.re * b.im_j - a.im_i * b.im_k + a.im_j * b.re + a.im_k * b.im_i
@[simp]
theorem quaternion.mul_im_k {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a * b).im_k = a.re * b.im_k + a.im_i * b.im_j - a.im_j * b.im_i + a.im_k * b.re
@[simp, norm_cast]
theorem quaternion.coe_mul {R : Type u_3} [comm_ring R] (x y : R) :
(x * y) = x * y
@[simp, norm_cast]
theorem quaternion.coe_pow {R : Type u_3} [comm_ring R] (x : R) (n : ) :
(x ^ n) = x ^ n
@[simp, norm_cast]
theorem quaternion.nat_cast_re {R : Type u_3} [comm_ring R] (n : ) :
@[simp, norm_cast]
theorem quaternion.nat_cast_im_i {R : Type u_3} [comm_ring R] (n : ) :
@[simp, norm_cast]
theorem quaternion.nat_cast_im_j {R : Type u_3} [comm_ring R] (n : ) :
@[simp, norm_cast]
theorem quaternion.nat_cast_im_k {R : Type u_3} [comm_ring R] (n : ) :
@[simp, norm_cast]
theorem quaternion.nat_cast_im {R : Type u_3} [comm_ring R] (n : ) :
n.im = 0
@[norm_cast]
theorem quaternion.coe_nat_cast {R : Type u_3} [comm_ring R] (n : ) :
@[simp, norm_cast]
theorem quaternion.int_cast_re {R : Type u_3} [comm_ring R] (z : ) :
@[simp, norm_cast]
theorem quaternion.int_cast_im_i {R : Type u_3} [comm_ring R] (z : ) :
@[simp, norm_cast]
theorem quaternion.int_cast_im_j {R : Type u_3} [comm_ring R] (z : ) :
@[simp, norm_cast]
theorem quaternion.int_cast_im_k {R : Type u_3} [comm_ring R] (z : ) :
@[simp, norm_cast]
theorem quaternion.int_cast_im {R : Type u_3} [comm_ring R] (z : ) :
z.im = 0
@[norm_cast]
theorem quaternion.coe_int_cast {R : Type u_3} [comm_ring R] (z : ) :
@[simp]
theorem quaternion.coe_inj {R : Type u_3} [comm_ring R] {x y : R} :
x = y x = y
@[simp]
theorem quaternion.smul_re {S : Type u_1} {R : Type u_3} [comm_ring R] (a : quaternion R) [has_smul S R] (s : S) :
(s a).re = s a.re
@[simp]
theorem quaternion.smul_im_i {S : Type u_1} {R : Type u_3} [comm_ring R] (a : quaternion R) [has_smul S R] (s : S) :
(s a).im_i = s a.im_i
@[simp]
theorem quaternion.smul_im_j {S : Type u_1} {R : Type u_3} [comm_ring R] (a : quaternion R) [has_smul S R] (s : S) :
(s a).im_j = s a.im_j
@[simp]
theorem quaternion.smul_im_k {S : Type u_1} {R : Type u_3} [comm_ring R] (a : quaternion R) [has_smul S R] (s : S) :
(s a).im_k = s a.im_k
@[simp]
theorem quaternion.smul_im {S : Type u_1} {R : Type u_3} [comm_ring R] (a : quaternion R) [smul_zero_class S R] (s : S) :
(s a).im = s a.im
@[simp, norm_cast]
theorem quaternion.coe_smul {S : Type u_1} {R : Type u_3} [comm_ring R] [smul_zero_class S R] (s : S) (r : R) :
(s r) = s r
theorem quaternion.coe_commutes {R : Type u_3} [comm_ring R] (r : R) (a : quaternion R) :
r * a = a * r
theorem quaternion.coe_commute {R : Type u_3} [comm_ring R] (r : R) (a : quaternion R) :
theorem quaternion.coe_mul_eq_smul {R : Type u_3} [comm_ring R] (r : R) (a : quaternion R) :
r * a = r a
theorem quaternion.mul_coe_eq_smul {R : Type u_3} [comm_ring R] (r : R) (a : quaternion R) :
a * r = r a
@[simp]
theorem quaternion.smul_coe {R : Type u_3} [comm_ring R] (x y : R) :
x y = (x * y)
@[protected, instance]
@[protected, instance]
@[simp]
theorem quaternion.star_re {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.star_im_i {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.star_im_j {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.star_im_k {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.star_im {R : Type u_3} [comm_ring R] (a : quaternion R) :
theorem quaternion.self_add_star' {R : Type u_3} [comm_ring R] (a : quaternion R) :
a + has_star.star a = (2 * a.re)
theorem quaternion.self_add_star {R : Type u_3} [comm_ring R] (a : quaternion R) :
a + has_star.star a = 2 * (a.re)
theorem quaternion.star_add_self' {R : Type u_3} [comm_ring R] (a : quaternion R) :
has_star.star a + a = (2 * a.re)
theorem quaternion.star_add_self {R : Type u_3} [comm_ring R] (a : quaternion R) :
has_star.star a + a = 2 * (a.re)
theorem quaternion.star_eq_two_re_sub {R : Type u_3} [comm_ring R] (a : quaternion R) :
has_star.star a = (2 * a.re) - a
@[simp, norm_cast]
theorem quaternion.star_coe {R : Type u_3} [comm_ring R] (x : R) :
@[simp]
theorem quaternion.im_star {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[simp]
theorem quaternion.star_smul {S : Type u_1} {R : Type u_3} [comm_ring R] [monoid S] [distrib_mul_action S R] (s : S) (a : quaternion R) :
theorem quaternion.eq_re_of_eq_coe {R : Type u_3} [comm_ring R] {a : quaternion R} {x : R} (h : a = x) :
a = (a.re)
@[simp]
theorem quaternion.star_eq_self {R : Type u_3} [comm_ring R] [no_zero_divisors R] [char_zero R] {a : quaternion R} :
@[simp]
theorem quaternion.star_eq_neg {R : Type u_3} [comm_ring R] [no_zero_divisors R] [char_zero R] {a : quaternion 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_3} [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_3} [comm_ring R] (x : R) :
@[norm_cast]
@[norm_cast]
theorem quaternion.im_sq {R : Type u_3} [comm_ring R] (a : quaternion R) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem quaternion.coe_inv {R : Type u_1} [linear_ordered_field R] (x : R) :
@[simp, norm_cast]
theorem quaternion.coe_div {R : Type u_1} [linear_ordered_field R] (x y : R) :
(x / y) = x / y
@[simp, norm_cast]
theorem quaternion.coe_zpow {R : Type u_1} [linear_ordered_field R] (x : R) (z : ) :
(x ^ z) = x ^ z
@[simp, norm_cast]
theorem quaternion.rat_cast_re {R : Type u_1} [linear_ordered_field R] (q : ) :
@[simp, norm_cast]
theorem quaternion.rat_cast_im_i {R : Type u_1} [linear_ordered_field R] (q : ) :
@[simp, norm_cast]
theorem quaternion.rat_cast_im_j {R : Type u_1} [linear_ordered_field R] (q : ) :
@[simp, norm_cast]
theorem quaternion.rat_cast_im_k {R : Type u_1} [linear_ordered_field R] (q : ) :
@[simp, norm_cast]
theorem quaternion.rat_cast_im {R : Type u_1} [linear_ordered_field R] (q : ) :
q.im = 0
@[norm_cast]
theorem quaternion.coe_rat_cast {R : Type u_1} [linear_ordered_field R] (q : ) :
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.