mathlib3 documentation

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:

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

Notation #

The following notation is available with open_locale quaternion:

Tags #

quaternion, normed ring, normed space, normed algebra

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

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

quaternion_algebra.linear_equiv_tuple as a linear_isometry_equiv.

Equations
@[continuity]
@[continuity]
@[continuity]
@[continuity]
@[continuity]
@[continuity]
@[protected, instance]
@[simp, norm_cast]
theorem quaternion.has_sum_coe {α : Type u_1} {f : α } {r : } :
has_sum (λ (a : α), (f a)) r has_sum f r
@[simp, norm_cast]
theorem quaternion.summable_coe {α : Type u_1} {f : α } :
summable (λ (a : α), (f a)) summable f
@[norm_cast]
theorem quaternion.tsum_coe {α : Type u_1} (f : α ) :
∑' (a : α), (f a) = ∑' (a : α), f a