mathlib documentation

analysis.quaternion

Quaternions as a normed algebra

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

Notation

The following notation is available with open_locale quaternion:

Tags

quaternion, normed ring, normed space, normed algebra

@[instance]

Equations
@[simp]
theorem quaternion.norm_mul (a b : ℍ[]) :

@[simp]

@[instance]

Equations
@[simp]
theorem quaternion.coe_complex_re (z : ) :
z.re = z.re

@[simp]
theorem quaternion.coe_complex_im_i (z : ) :

@[simp]
theorem quaternion.coe_complex_im_j (z : ) :

@[simp]
theorem quaternion.coe_complex_im_k (z : ) :

@[simp]
theorem quaternion.coe_complex_add (z w : ) :
(z + w) = z + w

@[simp]
theorem quaternion.coe_complex_mul (z w : ) :
z * w = (z) * w

@[simp]

@[simp]

@[simp]
theorem quaternion.coe_complex_smul (r : ) (z : ) :
(r z) = r z

@[simp]

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

Equations