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

source
theorem quaternion_algebra.ext {R : Type u_1} {a b : R} (x y : quaternion_algebra R a b) (h : x.re = y.re) (h_1 : x.im_i = y.im_i) (h_2 : x.im_j = y.im_j) (h_3 : x.im_k = y.im_k) :
x = y
source
theorem quaternion_algebra.ext_iff {R : Type u_1} {a b : R} (x y : quaternion_algebra R a b) :
x = y ↔ x.re = y.re ∧ x.im_i = y.im_i ∧ x.im_j = y.im_j ∧ x.im_k = y.im_k
source
@[nolint, ext]
structure quaternion_algebra (R : Type u_1) (a b : R) :
Type u_1
  • re : R
  • im_i : R
  • im_j : R
  • im_k : R

Quaternion algebra over a type with fixed coefficients $a=i^2$ and $b=j^2$. Implemented as a structure with four fields: re, im_i, im_j, and im_k.

Instances for quaternion_algebra
source
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_re {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
(⇑((quaternion_algebra.equiv_prod c₁ c₂).symm) a).re = a.fst
source
@[simp]
theorem quaternion_algebra.equiv_prod_apply {R : Type u_1} (c₁ c₂ : R) (a : quaternion_algebra R c₁ c₂) :
⇑(quaternion_algebra.equiv_prod c₁ c₂) a = (a.re, a.im_i, a.im_j, a.im_k)
source
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_im_i {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
(⇑((quaternion_algebra.equiv_prod c₁ c₂).symm) a).im_i = a.snd.fst
source
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_im_j {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
(⇑((quaternion_algebra.equiv_prod c₁ c₂).symm) a).im_j = a.snd.snd.fst
source
def quaternion_algebra.equiv_prod {R : Type u_1} (c₁ c₂ : R) :
quaternion_algebra R c₁ c₂ ≃ R × R × R × R

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

Equations
source
@[simp]
theorem quaternion_algebra.equiv_prod_symm_apply_im_k {R : Type u_1} (c₁ c₂ : R) (a : R × R × R × R) :
(⇑((quaternion_algebra.equiv_prod c₁ c₂).symm) a).im_k = a.snd.snd.snd
source
@[simp]
theorem quaternion_algebra.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}
source
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
source
@[simp]
theorem quaternion_algebra.equiv_tuple_apply {R : Type u_1} (c₁ c₂ : R) (x : quaternion_algebra R c₁ c₂) :
⇑(quaternion_algebra.equiv_tuple c₁ c₂) x = ![x.re, x.im_i, x.im_j, x.im_k]
source
@[simp]
theorem quaternion_algebra.mk.eta {R : Type u_1} {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
{re := a.re, im_i := a.im_i, im_j := a.im_j, im_k := a.im_k} = a
source
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
source
@[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
source
@[simp]
theorem quaternion_algebra.im_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
a.im.im_i = a.im_i
source
@[simp]
theorem quaternion_algebra.im_im_j {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
a.im.im_j = a.im_j
source
@[simp]
theorem quaternion_algebra.im_im_k {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
a.im.im_k = a.im_k
source
@[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
source
@[protected, instance]
def quaternion_algebra.has_coe_t {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
has_coe_t R (quaternion_algebra R c₁ c₂)
Equations
source
@[simp, norm_cast]
theorem quaternion_algebra.coe_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
↑x.re = x
source
@[simp, norm_cast]
theorem quaternion_algebra.coe_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
↑x.im_i = 0
source
@[simp, norm_cast]
theorem quaternion_algebra.coe_im_j {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
↑x.im_j = 0
source
@[simp, norm_cast]
theorem quaternion_algebra.coe_im_k {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
↑x.im_k = 0
source
theorem quaternion_algebra.coe_injective {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
function.injective coe
source
@[simp]
theorem quaternion_algebra.coe_inj {R : Type u_3} [comm_ring R] {c₁ c₂ x y : R} :
↑x = ↑y ↔ x = y
source
@[simp]
theorem quaternion_algebra.has_zero_zero_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
0.re = 0
source
@[simp]
theorem quaternion_algebra.has_zero_zero_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
0.im_i = 0
source
@[protected, instance]
def quaternion_algebra.has_zero {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
has_zero (quaternion_algebra R c₁ c₂)
Equations
source
@[simp]
theorem quaternion_algebra.has_zero_zero_im_k {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
0.im_k = 0
source
@[simp]
theorem quaternion_algebra.has_zero_zero_im_j {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
0.im_j = 0
source
@[simp, norm_cast]
theorem quaternion_algebra.coe_zero {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
↑0 = 0
source
@[protected, instance]
def quaternion_algebra.inhabited {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
inhabited (quaternion_algebra R c₁ c₂)
Equations
source
@[simp]
theorem quaternion_algebra.has_one_one_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
1.im_i = 0
source
@[protected, instance]
def quaternion_algebra.has_one {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
has_one (quaternion_algebra R c₁ c₂)
Equations
source
@[simp]
theorem quaternion_algebra.has_one_one_im_j {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
1.im_j = 0
source
@[simp]
theorem quaternion_algebra.has_one_one_im_k {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
1.im_k = 0
source
@[simp]
theorem quaternion_algebra.has_one_one_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
1.re = 1
source
@[simp, norm_cast]
theorem quaternion_algebra.coe_one {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
↑1 = 1
source
@[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
source
@[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
source
@[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
source
@[protected, instance]
def quaternion_algebra.has_add {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
has_add (quaternion_algebra R c₁ c₂)
Equations
source
@[simp]
theorem quaternion_algebra.has_add_add_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a b : quaternion_algebra R c₁ c₂) :
(a + b).re = a.re + b.re
source
@[simp]
theorem quaternion_algebra.mk_add_mk {R : Type u_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₄}
source
@[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
source
@[protected, instance]
def quaternion_algebra.has_neg {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
has_neg (quaternion_algebra R c₁ c₂)
Equations
source
@[simp]
theorem quaternion_algebra.has_neg_neg_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
(-a).im_i = -a.im_i
source
@[simp]
theorem quaternion_algebra.has_neg_neg_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
(-a).re = -a.re
source
@[simp]
theorem quaternion_algebra.has_neg_neg_im_j {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
(-a).im_j = -a.im_j
source
@[simp]
theorem quaternion_algebra.has_neg_neg_im_k {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
(-a).im_k = -a.im_k
source
@[simp]
theorem quaternion_algebra.neg_mk {R : Type u_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₄}
source
@[simp, norm_cast]
theorem quaternion_algebra.coe_neg {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
↑-x = -↑x
source
@[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
source
@[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
source
@[protected, instance]
def quaternion_algebra.has_sub {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
has_sub (quaternion_algebra R c₁ c₂)
Equations
source
@[simp]
theorem quaternion_algebra.has_sub_sub_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a b : quaternion_algebra R c₁ c₂) :
(a - b).im_i = a.im_i - b.im_i
source
@[simp]
theorem quaternion_algebra.has_sub_sub_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a b : quaternion_algebra R c₁ c₂) :
(a - b).re = a.re - b.re
source
@[simp]
theorem quaternion_algebra.mk_sub_mk {R : Type u_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₄}
source
@[simp, norm_cast]
theorem quaternion_algebra.coe_im {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
↑x.im = 0
source
@[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
source
@[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)
source
@[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
source
@[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
source
@[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
source
@[protected, instance]
def quaternion_algebra.has_mul {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
has_mul (quaternion_algebra R c₁ c₂)

Multiplication is given by

  • 1 * x = x * 1 = x;
  • i * i = c₁;
  • j * j = c₂;
  • i * j = k, j * i = -k;
  • k * k = -c₁ * c₂;
  • i * k = c₁ * j, k * i =-c₁ * j`;
  • j * k = -c₂ * i, `k * j = c₂ * i`.
Equations
source
@[simp]
theorem quaternion_algebra.has_mul_mul_im_j {R : Type u_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
source
@[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
source
@[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₁}
source
@[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] :
has_smul S (quaternion_algebra R c₁ c₂)
Equations
source
@[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] :
is_scalar_tower S T (quaternion_algebra R c₁ c₂)
source
@[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] :
smul_comm_class S T (quaternion_algebra R c₁ c₂)
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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}
source
@[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
source
@[protected, instance]
def quaternion_algebra.add_comm_group {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
add_comm_group (quaternion_algebra R c₁ c₂)
Equations
source
@[protected, instance]
def quaternion_algebra.add_group_with_one {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
add_group_with_one (quaternion_algebra R c₁ c₂)
Equations
source
@[simp, norm_cast]
theorem quaternion_algebra.nat_cast_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (n : ℕ) :
↑n.re = ↑n
source
@[simp, norm_cast]
theorem quaternion_algebra.nat_cast_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (n : ℕ) :
↑n.im_i = 0
source
@[simp, norm_cast]
theorem quaternion_algebra.nat_cast_im_j {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (n : ℕ) :
↑n.im_j = 0
source
@[simp, norm_cast]
theorem quaternion_algebra.nat_cast_im_k {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (n : ℕ) :
↑n.im_k = 0
source
@[simp, norm_cast]
theorem quaternion_algebra.nat_cast_im {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (n : ℕ) :
↑n.im = 0
source
@[norm_cast]
theorem quaternion_algebra.coe_nat_cast {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (n : ℕ) :
↑↑n = ↑n
source
@[simp, norm_cast]
theorem quaternion_algebra.int_cast_re {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (z : ℤ) :
↑z.re = ↑z
source
@[simp, norm_cast]
theorem quaternion_algebra.int_cast_im_i {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (z : ℤ) :
↑z.im_i = 0
source
@[simp, norm_cast]
theorem quaternion_algebra.int_cast_im_j {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (z : ℤ) :
↑z.im_j = 0
source
@[simp, norm_cast]
theorem quaternion_algebra.int_cast_im_k {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (z : ℤ) :
↑z.im_k = 0
source
@[simp, norm_cast]
theorem quaternion_algebra.int_cast_im {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (z : ℤ) :
↑z.im = 0
source
@[norm_cast]
theorem quaternion_algebra.coe_int_cast {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (z : ℤ) :
↑↑z = ↑z
source
@[protected, instance]
def quaternion_algebra.ring {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
ring (quaternion_algebra R c₁ c₂)
Equations
source
@[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
source
@[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
source
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}
source
def quaternion_algebra.re_lm {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
quaternion_algebra R c₁ c₂ →ₗ[R] R

quaternion_algebra.re as a linear_map

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

quaternion_algebra.im_i as a linear_map

Equations
source
@[simp]
theorem quaternion_algebra.im_i_lm_apply {R : Type u_3} [comm_ring R] (c₁ c₂ : R) (self : quaternion_algebra R c₁ c₂) :
⇑(quaternion_algebra.im_i_lm c₁ c₂) self = self.im_i
source
@[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
source
def quaternion_algebra.im_j_lm {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
quaternion_algebra R c₁ c₂ →ₗ[R] R

quaternion_algebra.im_j as a linear_map

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

quaternion_algebra.im_k as a linear_map

Equations
source
def quaternion_algebra.linear_equiv_tuple {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
quaternion_algebra R c₁ c₂ ≃ₗ[R] fin 4 → R

quaternion_algebra.equiv_tuple as a linear equivalence.

Equations
source
@[simp]
theorem quaternion_algebra.coe_linear_equiv_tuple {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
⇑(quaternion_algebra.linear_equiv_tuple c₁ c₂) = ⇑(quaternion_algebra.equiv_tuple c₁ c₂)
source
@[simp]
theorem quaternion_algebra.coe_linear_equiv_tuple_symm {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
⇑((quaternion_algebra.linear_equiv_tuple c₁ c₂).symm) = ⇑((quaternion_algebra.equiv_tuple c₁ c₂).symm)
source
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
source
@[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₂) :
⇑(⇑((quaternion_algebra.basis_one_i_j_k c₁ c₂).repr) q) = ![q.re, q.im_i, q.im_j, q.im_k]
source
@[protected, instance]
def quaternion_algebra.module.finite {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
module.finite R (quaternion_algebra R c₁ c₂)
source
@[protected, instance]
def quaternion_algebra.module.free {R : Type u_3} [comm_ring R] (c₁ c₂ : R) :
module.free R (quaternion_algebra R c₁ c₂)
source
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
source
theorem quaternion_algebra.finrank_eq_four {R : Type u_3} [comm_ring R] (c₁ c₂ : R) [strong_rank_condition R] :
finite_dimensional.finrank R (quaternion_algebra R c₁ c₂) = 4
source
@[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
source
@[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
source
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
source
theorem quaternion_algebra.coe_commute {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) :
commute ↑r a
source
theorem quaternion_algebra.coe_mul_eq_smul {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) :
↑r * a = r • a
source
theorem quaternion_algebra.mul_coe_eq_smul {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (r : R) (a : quaternion_algebra R c₁ c₂) :
a * ↑r = r • a
source
@[simp, norm_cast]
theorem quaternion_algebra.coe_algebra_map {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
⇑(algebra_map R (quaternion_algebra R c₁ c₂)) = coe
source
theorem quaternion_algebra.smul_coe {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x y : R) :
x • ↑y = ↑(x * y)
source
@[protected, instance]
def quaternion_algebra.has_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
has_star (quaternion_algebra R c₁ c₂)

Quaternion conjugate.

Equations
source
@[simp]
theorem quaternion_algebra.re_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
(has_star.star a).re = a.re
source
@[simp]
theorem quaternion_algebra.im_i_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
(has_star.star a).im_i = -a.im_i
source
@[simp]
theorem quaternion_algebra.im_j_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
(has_star.star a).im_j = -a.im_j
source
@[simp]
theorem quaternion_algebra.im_k_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
(has_star.star a).im_k = -a.im_k
source
@[simp]
theorem quaternion_algebra.im_star {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
(has_star.star a).im = -a.im
source
@[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₄}
source
@[protected, instance]
def quaternion_algebra.star_ring {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
star_ring (quaternion_algebra R c₁ c₂)
Equations
source
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)
source
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)
source
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)
source
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)
source
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
source
@[protected, instance]
def quaternion_algebra.is_star_normal {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
is_star_normal a
source
@[simp, norm_cast]
theorem quaternion_algebra.star_coe {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (x : R) :
has_star.star ↑x = ↑x
source
@[simp]
theorem quaternion_algebra.star_im {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
has_star.star a.im = -a.im
source
@[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₂) :
has_star.star (s • a) = s • has_star.star a
source
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)
source
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₂} :
a = ↑(a.re) ↔ a ∈ set.range coe
source
@[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₂} :
has_star.star a = a ↔ a = ↑(a.re)
source
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₂} :
has_star.star a = -a ↔ a.re = 0
source
theorem quaternion_algebra.star_mul_eq_coe {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
has_star.star a * a = ↑((has_star.star a * a).re)
source
theorem quaternion_algebra.mul_star_eq_coe {R : Type u_3} [comm_ring R] {c₁ c₂ : R} (a : quaternion_algebra R c₁ c₂) :
a * has_star.star a = ↑((a * has_star.star a).re)
source
def quaternion_algebra.star_ae {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
quaternion_algebra R c₁ c₂ ≃ₐ[R] (quaternion_algebra R c₁ c₂)ᵐᵒᵖ

Quaternion conjugate as an alg_equiv to the opposite ring.

Equations
source
@[simp]
theorem quaternion_algebra.coe_star_ae {R : Type u_3} [comm_ring R] {c₁ c₂ : R} :
⇑quaternion_algebra.star_ae = mul_opposite.op ∘ has_star.star
source
def quaternion (R : Type u_1) [has_one R] [has_neg R] :
Type u_1

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

Equations
Instances for quaternion
source
def quaternion.equiv_prod (R : Type u_1) [has_one R] [has_neg R] :
quaternion R ≃ R × R × R × R

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

Equations
source
@[simp]
theorem quaternion.equiv_prod_symm_apply_im_k (R : Type u_1) [has_one R] [has_neg R] (a : R × R × R × R) :
(⇑((quaternion.equiv_prod R).symm) a).im_k = a.snd.snd.snd
source
@[simp]
theorem quaternion.equiv_prod_apply (R : Type u_1) [has_one R] [has_neg R] (a : quaternion_algebra R (-1) (-1)) :
⇑(quaternion.equiv_prod R) a = (a.re, a.im_i, a.im_j, a.im_k)
source
@[simp]
theorem quaternion.equiv_prod_symm_apply_re (R : Type u_1) [has_one R] [has_neg R] (a : R × R × R × R) :
(⇑((quaternion.equiv_prod R).symm) a).re = a.fst
source
@[simp]
theorem quaternion.equiv_prod_symm_apply_im_j (R : Type u_1) [has_one R] [has_neg R] (a : R × R × R × R) :
(⇑((quaternion.equiv_prod R).symm) a).im_j = a.snd.snd.fst
source
@[simp]
theorem quaternion.equiv_prod_symm_apply_im_i (R : Type u_1) [has_one R] [has_neg R] (a : R × R × R × R) :
(⇑((quaternion.equiv_prod R).symm) a).im_i = a.snd.fst
source
@[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}
source
def quaternion.equiv_tuple (R : Type u_1) [has_one R] [has_neg R] :
quaternion R ≃ (fin 4 → R)

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

Equations
source
@[simp]
theorem quaternion.equiv_tuple_apply (R : Type u_1) [has_one R] [has_neg R] (x : quaternion R) :
⇑(quaternion.equiv_tuple R) x = ![x.re, x.im_i, x.im_j, x.im_k]
source
@[protected, instance]
def quaternion.has_coe_t {R : Type u_3} [comm_ring R] :
has_coe_t R (quaternion R)
Equations
source
@[protected, instance]
def quaternion.ring {R : Type u_3} [comm_ring R] :
ring (quaternion R)
Equations
source
@[protected, instance]
def quaternion.inhabited {R : Type u_3} [comm_ring R] :
inhabited (quaternion R)
Equations
source
@[protected, instance]
def quaternion.has_smul {S : Type u_1} {R : Type u_3} [comm_ring R] [has_smul S R] :
has_smul S (quaternion R)
Equations
source
@[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] :
is_scalar_tower S T (quaternion R)
source
@[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] :
smul_comm_class S T (quaternion R)
source
@[protected, instance]
def quaternion.algebra {S : Type u_1} {R : Type u_3} [comm_ring R] [comm_semiring S] [algebra S R] :
algebra S (quaternion R)
Equations
source
@[protected, instance]
def quaternion.star_ring {R : Type u_3} [comm_ring R] :
star_ring (quaternion R)
Equations
source
@[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
source
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
source
def quaternion.im {R : Type u_3} [comm_ring R] (x : quaternion R) :
quaternion R

The imaginary part of a quaternion.

Equations
source
@[simp]
theorem quaternion.im_re {R : Type u_3} [comm_ring R] (a : quaternion R) :
a.im.re = 0
source
@[simp]
theorem quaternion.im_im_i {R : Type u_3} [comm_ring R] (a : quaternion R) :
a.im.im_i = a.im_i
source
@[simp]
theorem quaternion.im_im_j {R : Type u_3} [comm_ring R] (a : quaternion R) :
a.im.im_j = a.im_j
source
@[simp]
theorem quaternion.im_im_k {R : Type u_3} [comm_ring R] (a : quaternion R) :
a.im.im_k = a.im_k
source
@[simp]
theorem quaternion.im_idem {R : Type u_3} [comm_ring R] (a : quaternion R) :
a.im.im = a.im
source
@[simp]
theorem quaternion.re_add_im {R : Type u_3} [comm_ring R] (a : quaternion R) :
↑(a.re) + a.im = a
source
@[simp]
theorem quaternion.sub_self_im {R : Type u_3} [comm_ring R] (a : quaternion R) :
a - a.im = ↑(a.re)
source
@[simp]
theorem quaternion.sub_self_re {R : Type u_3} [comm_ring R] (a : quaternion R) :
a - ↑(a.re) = a.im
source
@[simp, norm_cast]
theorem quaternion.coe_re {R : Type u_3} [comm_ring R] (x : R) :
↑x.re = x
source
@[simp, norm_cast]
theorem quaternion.coe_im_i {R : Type u_3} [comm_ring R] (x : R) :
↑x.im_i = 0
source
@[simp, norm_cast]
theorem quaternion.coe_im_j {R : Type u_3} [comm_ring R] (x : R) :
↑x.im_j = 0
source
@[simp, norm_cast]
theorem quaternion.coe_im_k {R : Type u_3} [comm_ring R] (x : R) :
↑x.im_k = 0
source
@[simp, norm_cast]
theorem quaternion.coe_im {R : Type u_3} [comm_ring R] (x : R) :
↑x.im = 0
source
@[simp]
theorem quaternion.zero_re {R : Type u_3} [comm_ring R] :
0.re = 0
source
@[simp]
theorem quaternion.zero_im_i {R : Type u_3} [comm_ring R] :
0.im_i = 0
source
@[simp]
theorem quaternion.zero_im_j {R : Type u_3} [comm_ring R] :
0.im_j = 0
source
@[simp]
theorem quaternion.zero_im_k {R : Type u_3} [comm_ring R] :
0.im_k = 0
source
@[simp]
theorem quaternion.zero_im {R : Type u_3} [comm_ring R] :
0.im = 0
source
@[simp, norm_cast]
theorem quaternion.coe_zero {R : Type u_3} [comm_ring R] :
↑0 = 0
source
@[simp]
theorem quaternion.one_re {R : Type u_3} [comm_ring R] :
1.re = 1
source
@[simp]
theorem quaternion.one_im_i {R : Type u_3} [comm_ring R] :
1.im_i = 0
source
@[simp]
theorem quaternion.one_im_j {R : Type u_3} [comm_ring R] :
1.im_j = 0
source
@[simp]
theorem quaternion.one_im_k {R : Type u_3} [comm_ring R] :
1.im_k = 0
source
@[simp]
theorem quaternion.one_im {R : Type u_3} [comm_ring R] :
1.im = 0
source
@[simp, norm_cast]
theorem quaternion.coe_one {R : Type u_3} [comm_ring R] :
↑1 = 1
source
@[simp]
theorem quaternion.add_re {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a + b).re = a.re + b.re
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem quaternion.add_im {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a + b).im = a.im + b.im
source
@[simp, norm_cast]
theorem quaternion.coe_add {R : Type u_3} [comm_ring R] (x y : R) :
↑(x + y) = ↑x + ↑y
source
@[simp]
theorem quaternion.neg_re {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).re = -a.re
source
@[simp]
theorem quaternion.neg_im_i {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).im_i = -a.im_i
source
@[simp]
theorem quaternion.neg_im_j {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).im_j = -a.im_j
source
@[simp]
theorem quaternion.neg_im_k {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).im_k = -a.im_k
source
@[simp]
theorem quaternion.neg_im {R : Type u_3} [comm_ring R] (a : quaternion R) :
(-a).im = -a.im
source
@[simp, norm_cast]
theorem quaternion.coe_neg {R : Type u_3} [comm_ring R] (x : R) :
↑-x = -↑x
source
@[simp]
theorem quaternion.sub_re {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a - b).re = a.re - b.re
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem quaternion.sub_im {R : Type u_3} [comm_ring R] (a b : quaternion R) :
(a - b).im = a.im - b.im
source
@[simp, norm_cast]
theorem quaternion.coe_sub {R : Type u_3} [comm_ring R] (x y : R) :
↑(x - y) = ↑x - ↑y
source
@[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
source
@[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
source
@[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
source
@[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
source
@[simp, norm_cast]
theorem quaternion.coe_mul {R : Type u_3} [comm_ring R] (x y : R) :
↑(x * y) = ↑x * ↑y
source
@[simp, norm_cast]
theorem quaternion.coe_pow {R : Type u_3} [comm_ring R] (x : R) (n : ℕ) :
↑(x ^ n) = ↑x ^ n
source
@[simp, norm_cast]
theorem quaternion.nat_cast_re {R : Type u_3} [comm_ring R] (n : ℕ) :
↑n.re = ↑n
source
@[simp, norm_cast]
theorem quaternion.nat_cast_im_i {R : Type u_3} [comm_ring R] (n : ℕ) :
↑n.im_i = 0
source
@[simp, norm_cast]
theorem quaternion.nat_cast_im_j {R : Type u_3} [comm_ring R] (n : ℕ) :
↑n.im_j = 0
source
@[simp, norm_cast]
theorem quaternion.nat_cast_im_k {R : Type u_3} [comm_ring R] (n : ℕ) :
↑n.im_k = 0
source
@[simp, norm_cast]
theorem quaternion.nat_cast_im {R : Type u_3} [comm_ring R] (n : ℕ) :
↑n.im = 0
source
@[norm_cast]
theorem quaternion.coe_nat_cast {R : Type u_3} [comm_ring R] (n : ℕ) :
↑↑n = ↑n
source
@[simp, norm_cast]
theorem quaternion.int_cast_re {R : Type u_3} [comm_ring R] (z : ℤ) :
↑z.re = ↑z
source
@[simp, norm_cast]
theorem quaternion.int_cast_im_i {R : Type u_3} [comm_ring R] (z : ℤ) :
↑z.im_i = 0
source
@[simp, norm_cast]
theorem quaternion.int_cast_im_j {R : Type u_3} [comm_ring R] (z : ℤ) :
↑z.im_j = 0
source
@[simp, norm_cast]
theorem quaternion.int_cast_im_k {R : Type u_3} [comm_ring R] (z : ℤ) :
↑z.im_k = 0
source
@[simp, norm_cast]
theorem quaternion.int_cast_im {R : Type u_3} [comm_ring R] (z : ℤ) :
↑z.im = 0
source
@[norm_cast]
theorem quaternion.coe_int_cast {R : Type u_3} [comm_ring R] (z : ℤ) :
↑↑z = ↑z
source
theorem quaternion.coe_injective {R : Type u_3} [comm_ring R] :
function.injective coe
source
@[simp]
theorem quaternion.coe_inj {R : Type u_3} [comm_ring R] {x y : R} :
↑x = ↑y ↔ x = y
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem quaternion.coe_commutes {R : Type u_3} [comm_ring R] (r : R) (a : quaternion R) :
↑r * a = a * ↑r
source
theorem quaternion.coe_commute {R : Type u_3} [comm_ring R] (r : R) (a : quaternion R) :
commute ↑r a
source
theorem quaternion.coe_mul_eq_smul {R : Type u_3} [comm_ring R] (r : R) (a : quaternion R) :
↑r * a = r • a
source
theorem quaternion.mul_coe_eq_smul {R : Type u_3} [comm_ring R] (r : R) (a : quaternion R) :
a * ↑r = r • a
source
@[simp]
theorem quaternion.algebra_map_def {R : Type u_3} [comm_ring R] :
⇑(algebra_map R (quaternion R)) = coe
source
theorem quaternion.smul_coe {R : Type u_3} [comm_ring R] (x y : R) :
x • ↑y = ↑(x * y)
source
@[protected, instance]
def quaternion.module.finite {R : Type u_3} [comm_ring R] :
module.finite R (quaternion R)
source
@[protected, instance]
def quaternion.module.free {R : Type u_3} [comm_ring R] :
module.free R (quaternion R)
source
theorem quaternion.rank_eq_four {R : Type u_3} [comm_ring R] [strong_rank_condition R] :
module.rank R (quaternion R) = 4
source
theorem quaternion.finrank_eq_four {R : Type u_3} [comm_ring R] [strong_rank_condition R] :
finite_dimensional.finrank R (quaternion R) = 4
source
@[simp]
theorem quaternion.star_re {R : Type u_3} [comm_ring R] (a : quaternion R) :
(has_star.star a).re = a.re
source
@[simp]
theorem quaternion.star_im_i {R : Type u_3} [comm_ring R] (a : quaternion R) :
(has_star.star a).im_i = -a.im_i
source
@[simp]
theorem quaternion.star_im_j {R : Type u_3} [comm_ring R] (a : quaternion R) :
(has_star.star a).im_j = -a.im_j
source
@[simp]
theorem quaternion.star_im_k {R : Type u_3} [comm_ring R] (a : quaternion R) :
(has_star.star a).im_k = -a.im_k
source
@[simp]
theorem quaternion.star_im {R : Type u_3} [comm_ring R] (a : quaternion R) :
(has_star.star a).im = -a.im
source
theorem quaternion.self_add_star' {R : Type u_3} [comm_ring R] (a : quaternion R) :
a + has_star.star a = ↑(2 * a.re)
source
theorem quaternion.self_add_star {R : Type u_3} [comm_ring R] (a : quaternion R) :
a + has_star.star a = 2 * ↑(a.re)
source
theorem quaternion.star_add_self' {R : Type u_3} [comm_ring R] (a : quaternion R) :
has_star.star a + a = ↑(2 * a.re)
source
theorem quaternion.star_add_self {R : Type u_3} [comm_ring R] (a : quaternion R) :
has_star.star a + a = 2 * ↑(a.re)
source
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
source
@[simp, norm_cast]
theorem quaternion.star_coe {R : Type u_3} [comm_ring R] (x : R) :
has_star.star ↑x = ↑x
source
@[simp]
theorem quaternion.im_star {R : Type u_3} [comm_ring R] (a : quaternion R) :
has_star.star a.im = -a.im
source
@[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) :
has_star.star (s • a) = s • has_star.star a
source
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)
source
theorem quaternion.eq_re_iff_mem_range_coe {R : Type u_3} [comm_ring R] {a : quaternion R} :
a = ↑(a.re) ↔ a ∈ set.range coe
source
@[simp]
theorem quaternion.star_eq_self {R : Type u_3} [comm_ring R] [no_zero_divisors R] [char_zero R] {a : quaternion R} :
has_star.star a = a ↔ a = ↑(a.re)
source
@[simp]
theorem quaternion.star_eq_neg {R : Type u_3} [comm_ring R] [no_zero_divisors R] [char_zero R] {a : quaternion R} :
has_star.star a = -a ↔ a.re = 0
source
theorem quaternion.star_mul_eq_coe {R : Type u_3} [comm_ring R] (a : quaternion R) :
has_star.star a * a = ↑((has_star.star a * a).re)
source
theorem quaternion.mul_star_eq_coe {R : Type u_3} [comm_ring R] (a : quaternion R) :
a * has_star.star a = ↑((a * has_star.star a).re)
source
def quaternion.star_ae {R : Type u_3} [comm_ring R] :
quaternion R ≃ₐ[R] (quaternion R)ᵐᵒᵖ

Quaternion conjugate as an alg_equiv to the opposite ring.

Equations
source
@[simp]
theorem quaternion.coe_star_ae {R : Type u_3} [comm_ring R] :
⇑quaternion.star_ae = mul_opposite.op ∘ has_star.star
source
def quaternion.norm_sq {R : Type u_3} [comm_ring R] :
quaternion R →*₀ R

Square of the norm.

Equations
source
theorem quaternion.norm_sq_def {R : Type u_3} [comm_ring R] (a : quaternion R) :
⇑quaternion.norm_sq a = (a * has_star.star a).re
source
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
source
theorem quaternion.norm_sq_coe {R : Type u_3} [comm_ring R] (x : R) :
⇑quaternion.norm_sq ↑x = x ^ 2
source
@[simp]
theorem quaternion.norm_sq_star {R : Type u_3} [comm_ring R] (a : quaternion R) :
⇑quaternion.norm_sq (has_star.star a) = ⇑quaternion.norm_sq a
source
@[norm_cast]
theorem quaternion.norm_sq_nat_cast {R : Type u_3} [comm_ring R] (n : ℕ) :
⇑quaternion.norm_sq ↑n = ↑n ^ 2
source
@[norm_cast]
theorem quaternion.norm_sq_int_cast {R : Type u_3} [comm_ring R] (z : ℤ) :
⇑quaternion.norm_sq ↑z = ↑z ^ 2
source
@[simp]
theorem quaternion.norm_sq_neg {R : Type u_3} [comm_ring R] (a : quaternion R) :
⇑quaternion.norm_sq (-a) = ⇑quaternion.norm_sq a
source
theorem quaternion.self_mul_star {R : Type u_3} [comm_ring R] (a : quaternion R) :
a * has_star.star a = ↑(⇑quaternion.norm_sq a)
source
theorem quaternion.star_mul_self {R : Type u_3} [comm_ring R] (a : quaternion R) :
has_star.star a * a = ↑(⇑quaternion.norm_sq a)
source
theorem quaternion.im_sq {R : Type u_3} [comm_ring R] (a : quaternion R) :
a.im ^ 2 = -↑(⇑quaternion.norm_sq a.im)
source
theorem quaternion.coe_norm_sq_add {R : Type u_3} [comm_ring R] (a b : quaternion R) :
↑(⇑quaternion.norm_sq (a + b)) = ↑(⇑quaternion.norm_sq a) + a * has_star.star b + b * has_star.star a + ↑(⇑quaternion.norm_sq b)
source
theorem quaternion.norm_sq_smul {R : Type u_3} [comm_ring R] (r : R) (q : quaternion R) :
⇑quaternion.norm_sq (r • q) = r ^ 2 * ⇑quaternion.norm_sq q
source
theorem quaternion.norm_sq_add {R : Type u_3} [comm_ring R] (a b : quaternion R) :
⇑quaternion.norm_sq (a + b) = ⇑quaternion.norm_sq a + ⇑quaternion.norm_sq b + 2 * (a * has_star.star b).re
source
@[simp]
theorem quaternion.norm_sq_eq_zero {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} :
⇑quaternion.norm_sq a = 0 ↔ a = 0
source
theorem quaternion.norm_sq_ne_zero {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} :
⇑quaternion.norm_sq a ≠ 0 ↔ a ≠ 0
source
@[simp]
theorem quaternion.norm_sq_nonneg {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} :
0 ≤ ⇑quaternion.norm_sq a
source
@[simp]
theorem quaternion.norm_sq_le_zero {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} :
⇑quaternion.norm_sq a ≤ 0 ↔ a = 0
source
@[protected, instance]
def quaternion.nontrivial {R : Type u_1} [linear_ordered_comm_ring R] :
nontrivial (quaternion R)
source
@[protected, instance]
def quaternion.no_zero_divisors {R : Type u_1} [linear_ordered_comm_ring R] :
no_zero_divisors (quaternion R)
source
@[protected, instance]
def quaternion.is_domain {R : Type u_1} [linear_ordered_comm_ring R] :
is_domain (quaternion R)
source
theorem quaternion.sq_eq_norm_sq {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} :
a ^ 2 = ↑(⇑quaternion.norm_sq a) ↔ a = ↑(a.re)
source
theorem quaternion.sq_eq_neg_norm_sq {R : Type u_1} [linear_ordered_comm_ring R] {a : quaternion R} :
a ^ 2 = -↑(⇑quaternion.norm_sq a) ↔ a.re = 0
source
@[protected, instance]
def quaternion.has_inv {R : Type u_1} [linear_ordered_field R] :
has_inv (quaternion R)
Equations
source
theorem quaternion.has_inv_inv {R : Type u_1} [linear_ordered_field R] (a : quaternion R) :
a⁻¹ = (⇑quaternion.norm_sq a)⁻¹ • has_star.star a
source
@[protected, instance]
def quaternion.group_with_zero {R : Type u_1} [linear_ordered_field R] :
group_with_zero (quaternion R)
Equations
source
@[simp, norm_cast]
theorem quaternion.coe_inv {R : Type u_1} [linear_ordered_field R] (x : R) :
↑x⁻¹ = (↑x)⁻¹
source
@[simp, norm_cast]
theorem quaternion.coe_div {R : Type u_1} [linear_ordered_field R] (x y : R) :
↑(x / y) = ↑x / ↑y
source
@[simp, norm_cast]
theorem quaternion.coe_zpow {R : Type u_1} [linear_ordered_field R] (x : R) (z : ℤ) :
↑(x ^ z) = ↑x ^ z
source
@[protected, instance]
def quaternion.division_ring {R : Type u_1} [linear_ordered_field R] :
division_ring (quaternion R)
Equations
source
@[simp, norm_cast]
theorem quaternion.rat_cast_re {R : Type u_1} [linear_ordered_field R] (q : ℚ) :
↑q.re = ↑q
source
@[simp, norm_cast]
theorem quaternion.rat_cast_im_i {R : Type u_1} [linear_ordered_field R] (q : ℚ) :
↑q.im_i = 0
source
@[simp, norm_cast]
theorem quaternion.rat_cast_im_j {R : Type u_1} [linear_ordered_field R] (q : ℚ) :
↑q.im_j = 0
source
@[simp, norm_cast]
theorem quaternion.rat_cast_im_k {R : Type u_1} [linear_ordered_field R] (q : ℚ) :
↑q.im_k = 0
source
@[simp, norm_cast]
theorem quaternion.rat_cast_im {R : Type u_1} [linear_ordered_field R] (q : ℚ) :
↑q.im = 0
source
@[norm_cast]
theorem quaternion.coe_rat_cast {R : Type u_1} [linear_ordered_field R] (q : ℚ) :
↑↑q = ↑q
source
@[simp]
theorem quaternion.norm_sq_inv {R : Type u_1} [linear_ordered_field R] (a : quaternion R) :
⇑quaternion.norm_sq a⁻¹ = (⇑quaternion.norm_sq a)⁻¹
source
@[simp]
theorem quaternion.norm_sq_div {R : Type u_1} [linear_ordered_field R] (a b : quaternion R) :
⇑quaternion.norm_sq (a / b) = ⇑quaternion.norm_sq a / ⇑quaternion.norm_sq b
source
@[simp]
theorem quaternion.norm_sq_zpow {R : Type u_1} [linear_ordered_field R] (a : quaternion R) (z : ℤ) :
⇑quaternion.norm_sq (a ^ z) = ⇑quaternion.norm_sq a ^ z
source
@[norm_cast]
theorem quaternion.norm_sq_rat_cast {R : Type u_1} [linear_ordered_field R] (q : ℚ) :
⇑quaternion.norm_sq ↑q = ↑q ^ 2
source
theorem cardinal.mk_quaternion_algebra {R : Type u_1} (c₁ c₂ : R) :
cardinal.mk (quaternion_algebra R c₁ c₂) = cardinal.mk R ^ 4

The cardinality of a quaternion algebra, as a type.

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

The cardinality of a quaternion algebra, as a set.

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

The cardinality of the quaternions, as a type.

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

The cardinality of the quaternions, as a set.

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