Quaternions as a normed algebra #
In this file we define the following structures on the space ℍ := ℍ[ℝ]
of quaternions:
- inner product space;
- normed ring;
- normed space over
ℝ
.
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
:
ℍ
: quaternions
Tags #
quaternion, normed ring, normed space, normed algebra
Coercion ℂ →ₐ[ℝ] ℍ
as an algebra homomorphism.
Instances For
theorem
Quaternion.norm_piLp_equiv_symm_equivTuple
(x : Quaternion ℝ)
:
‖↑(WithLp.equiv 2 (Fin 4 → ℝ)).symm (↑(Quaternion.equivTuple ℝ) x)‖ = ‖x‖
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))
:
↑(LinearIsometryEquiv.symm Quaternion.linearIsometryEquivTuple) a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }
QuaternionAlgebra.linearEquivTuple
as a LinearIsometryEquiv
.