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

Space of quaternions over a type. Implemented as a structure with four fields: re, im_i, im_j, and im_k.

Equations
Instances For
    Equations
    theorem Quaternion.inner_self (a : Quaternion ) :
    a, a⟫_ = Quaternion.normSq a
    theorem Quaternion.inner_def (a : Quaternion ) (b : Quaternion ) :
    a, b⟫_ = (a * star b).re
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Quaternion.norm_coe (a : ) :

    Coercion from to .

    Equations
    • z = { re := z.re, imI := z.im, imJ := 0, imK := 0 }
    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.

      Equations
      • One or more equations did not get rendered due to their size.
      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.linearIsometryEquivTuple_symm_apply (a : EuclideanSpace (Fin 4)) :
        Quaternion.linearIsometryEquivTuple.symm a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }

        QuaternionAlgebra.linearEquivTuple as a LinearIsometryEquiv.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          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)