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
ℝ
.
Notation #
The following notation is available with open_locale quaternion
:
ℍ
: quaternions
Tags #
quaternion, normed ring, normed space, normed algebra
@[protected, instance]
Equations
- quaternion.has_inner = {inner := λ (a b : quaternion ℝ), (a * ⇑quaternion.conj b).re}
theorem
quaternion.inner_def
(a b : quaternion ℝ) :
has_inner.inner a b = (a * ⇑quaternion.conj b).re
@[protected, instance]
Equations
- quaternion.inner_product_space = inner_product_space.of_core {inner := has_inner.inner quaternion.has_inner, conj_sym := quaternion.inner_product_space._proof_1, nonneg_re := quaternion.inner_product_space._proof_2, definite := quaternion.inner_product_space._proof_3, add_left := quaternion.inner_product_space._proof_4, smul_left := quaternion.inner_product_space._proof_5}
@[protected, instance]
Equations
- quaternion.normed_division_ring = {to_has_norm := normed_add_comm_group.to_has_norm (inner_product_space.to_normed_add_comm_group ℝ), to_division_ring := quaternion.division_ring real.linear_ordered_field, to_metric_space := normed_add_comm_group.to_metric_space (inner_product_space.to_normed_add_comm_group ℝ), dist_eq := quaternion.normed_division_ring._proof_1, norm_mul' := quaternion.normed_division_ring._proof_2}
@[protected, instance]
Equations
- quaternion.normed_algebra = {to_algebra := quaternion.algebra real.comm_ring, norm_smul_le := quaternion.normed_algebra._proof_1}
Coercion ℂ →ₐ[ℝ] ℍ
as an algebra homomorphism.
Equations
- quaternion.of_complex = {to_fun := coe coe_to_lift, map_one' := quaternion.of_complex._proof_1, map_mul' := quaternion.coe_complex_mul, map_zero' := quaternion.of_complex._proof_2, map_add' := quaternion.coe_complex_add, commutes' := quaternion.of_complex._proof_3}