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_real_complex_mul (r : ) (z : ) :
r z = (r) * z
@[simp]

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

Equations