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

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