# mathlib3documentation

analysis.quaternion

# Quaternions as a normed algebra #

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

In this file we define the following structures on the space ℍ := ℍ[ℝ] of quaternions:

• inner product space;
• normed ring;
• normed space over ℝ.

We show that the norm on ℍ[ℝ] agrees with the euclidean norm of its components.

## Notation #

The following notation is available with open_locale quaternion:

• ℍ : quaternions

## Tags #

quaternion, normed ring, normed space, normed algebra

@[protected, instance]
Equations
theorem quaternion.inner_def (a b : quaternion ) :
= (a * .re
@[protected, instance]
Equations
@[protected, instance]
noncomputable def quaternion.inner_product_space  :
Equations
@[protected, instance]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp]
@[simp]
@[protected, instance]
noncomputable def quaternion.normed_division_ring  :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[simp, norm_cast]
theorem quaternion.coe_complex_re (z : ) :
z.re = z.re
@[simp, norm_cast]
theorem quaternion.coe_complex_im_i (z : ) :
@[simp, norm_cast]
theorem quaternion.coe_complex_im_j (z : ) :
@[simp, norm_cast]
theorem quaternion.coe_complex_im_k (z : ) :
@[simp, norm_cast]
theorem quaternion.coe_complex_add (z w : ) :
(z + w) = z + w
@[simp, norm_cast]
theorem quaternion.coe_complex_mul (z w : ) :
(z * w) = z * w
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
theorem quaternion.coe_real_complex_mul (r : ) (z : ) :
r z = r * z
@[simp, norm_cast]

Coercion ℂ →ₐ[ℝ] ℍ as an algebra homomorphism.

Equations
@[simp]

The norm of the components as a euclidean vector equals the norm of the quaternion.

@[simp]
theorem quaternion.linear_isometry_equiv_tuple_symm_apply (a : (fin 4)) :
= {re := a 0, im_i := a 1, im_j := a 2, im_k := a 3}
@[simp]

quaternion_algebra.linear_equiv_tuple as a linear_isometry_equiv.

Equations
@[continuity]
@[continuity]
@[continuity]
theorem quaternion.continuous_re  :
continuous (λ (q : , q.re)
@[continuity]
theorem quaternion.continuous_im_i  :
continuous (λ (q : , q.im_i)
@[continuity]
theorem quaternion.continuous_im_j  :
continuous (λ (q : , q.im_j)
@[continuity]
theorem quaternion.continuous_im_k  :
continuous (λ (q : , q.im_k)
@[continuity]
theorem quaternion.continuous_im  :
continuous (λ (q : , q.im)
@[protected, instance]
@[simp, norm_cast]
theorem quaternion.has_sum_coe {α : Type u_1} {f : α } {r : } :
has_sum (λ (a : α), (f a)) r r
@[simp, norm_cast]
theorem quaternion.summable_coe {α : Type u_1} {f : α } :
summable (λ (a : α), (f a))
@[norm_cast]
theorem quaternion.tsum_coe {α : Type u_1} (f : α ) :
∑' (a : α), (f a) = ∑' (a : α), f a