Documentation

Mathlib.Analysis.Quaternion

Quaternions as a normed algebra #

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 Quaternion or open scoped Quaternion:

Tags #

quaternion, normed ring, normed space, normed algebra

theorem Quaternion.inner_self (a : Quaternion ) :
inner a a = Quaternion.normSq a
theorem Quaternion.inner_def (a : Quaternion ) (b : Quaternion ) :
inner a b = (a * star b).re
theorem Quaternion.normSq_eq_norm_mul_self (a : Quaternion ) :
Quaternion.normSq a = a * a
@[simp]
theorem Quaternion.norm_coe (a : ) :

Coercion from to .

Instances For
    @[simp]
    theorem Quaternion.coeComplex_re (z : ) :
    (z).re = z.re
    @[simp]
    theorem Quaternion.coeComplex_imI (z : ) :
    (z).imI = z.im
    @[simp]
    theorem Quaternion.coeComplex_imJ (z : ) :
    (z).imJ = 0
    @[simp]
    theorem Quaternion.coeComplex_imK (z : ) :
    (z).imK = 0
    @[simp]
    theorem Quaternion.coeComplex_add (z : ) (w : ) :
    ↑(z + w) = z + w
    @[simp]
    theorem Quaternion.coeComplex_mul (z : ) (w : ) :
    ↑(z * w) = z * w
    @[simp]
    @[simp]
    @[simp]
    theorem Quaternion.coe_real_complex_mul (r : ) (z : ) :
    ↑(r z) = r * z
    @[simp]
    theorem Quaternion.coeComplex_coe (r : ) :
    r = r

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

    Instances For

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

      @[simp]
      theorem Quaternion.linearIsometryEquivTuple_apply (a : Quaternion ) :
      Quaternion.linearIsometryEquivTuple a = (WithLp.equiv 2 (Fin 4)).symm ![a.re, a.imI, a.imJ, a.imK]
      @[simp]
      theorem Quaternion.continuous_normSq :
      Continuous Quaternion.normSq
      @[simp]
      theorem Quaternion.hasSum_coe {α : Type u_1} {f : α} {r : } :
      HasSum (fun a => ↑(f a)) r HasSum f r
      @[simp]
      theorem Quaternion.summable_coe {α : Type u_1} {f : α} :
      (Summable fun a => ↑(f a)) Summable f
      theorem Quaternion.tsum_coe {α : Type u_1} (f : α) :
      ∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)