Quaternions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define quaternions ℍ[R] over a commutative ring R, and define some
algebraic structures on ℍ[R].
Main definitions #
quaternion_algebra R a b,ℍ[R, a, b]: quaternion algebra with coefficientsa,bquaternion R,ℍ[R]: the space of quaternions, a.k.a.quaternion_algebra R (-1) (-1);quaternion.norm_sq: square of the norm of a quaternion;quaternion.star_ring: provides the conjugate of a quaternion ashas_star.star;
We also define the following algebraic structures on ℍ[R]:
ring ℍ[R, a, b]andalgebra R ℍ[R, a, b]: for any commutative ringR;ring ℍ[R]andalgebra R ℍ[R]: for any commutative ringR;domain ℍ[R]: for a linear ordered commutative ringR;division_algebra ℍ[R]: for a linear ordered fieldR.
Notation #
The following notation is available with open_locale quaternion.
ℍ[R, c₁, c₂]:quaternion_algebra R c₁ c₂ℍ[R]: quaternions overR.
Implementation notes #
We define quaternions over any ring R, not just ℝ to be able to deal with, e.g., integer
or rational quaternions without using real numbers. In particular, all definitions in this file
are computable.
Tags #
quaternion
@[nolint, ext]
- re : R
- im_i : R
- im_j : R
- im_k : R
Quaternion algebra over a type with fixed coefficients $a=i^2$ and $b=j^2$.
Implemented as a structure with four fields: re, im_i, im_j, and im_k.
Instances for quaternion_algebra
- quaternion_algebra.has_sizeof_inst
- quaternion_algebra.has_coe_t
- quaternion_algebra.has_zero
- quaternion_algebra.inhabited
- quaternion_algebra.has_one
- quaternion_algebra.has_add
- quaternion_algebra.has_neg
- quaternion_algebra.has_sub
- quaternion_algebra.has_mul
- quaternion_algebra.has_smul
- quaternion_algebra.is_scalar_tower
- quaternion_algebra.smul_comm_class
- quaternion_algebra.add_comm_group
- quaternion_algebra.add_group_with_one
- quaternion_algebra.ring
- quaternion_algebra.algebra
- quaternion_algebra.module.finite
- quaternion_algebra.module.free
- quaternion_algebra.has_star
- quaternion_algebra.star_ring
@[simp]
theorem
quaternion_algebra.equiv_prod_apply
{R : Type u_1}
(c₁ c₂ : R)
(a : quaternion_algebra R c₁ c₂) :
def
quaternion_algebra.equiv_prod
{R : Type u_1}
(c₁ c₂ : R) :
quaternion_algebra R c₁ c₂ ≃ R × R × R × R
The equivalence between a quaternion algebra over R and R × R × R × R.
def
quaternion_algebra.equiv_tuple
{R : Type u_1}
(c₁ c₂ : R) :
quaternion_algebra R c₁ c₂ ≃ (fin 4 → R)
The equivalence between a quaternion algebra over R and fin 4 → R.
@[simp]
theorem
quaternion_algebra.equiv_tuple_apply
{R : Type u_1}
(c₁ c₂ : R)
(x : quaternion_algebra R c₁ c₂) :
@[simp]
theorem
quaternion_algebra.im_re
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem
quaternion_algebra.im_im_i
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem
quaternion_algebra.im_im_j
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem
quaternion_algebra.im_im_k
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem
quaternion_algebra.im_idem
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[protected, instance]
def
quaternion_algebra.has_coe_t
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
has_coe_t R (quaternion_algebra R c₁ c₂)
@[protected, instance]
def
quaternion_algebra.has_zero
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
has_zero (quaternion_algebra R c₁ c₂)
@[protected, instance]
def
quaternion_algebra.inhabited
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
inhabited (quaternion_algebra R c₁ c₂)
Equations
@[protected, instance]
def
quaternion_algebra.has_one
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
has_one (quaternion_algebra R c₁ c₂)
@[protected, instance]
def
quaternion_algebra.has_add
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
has_add (quaternion_algebra R c₁ c₂)
@[simp]
theorem
quaternion_algebra.has_neg_neg_im_i
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem
quaternion_algebra.has_neg_neg_re
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem
quaternion_algebra.has_neg_neg_im_j
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem
quaternion_algebra.has_neg_neg_im_k
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[protected, instance]
def
quaternion_algebra.has_sub
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
has_sub (quaternion_algebra R c₁ c₂)
@[simp]
theorem
quaternion_algebra.re_add_im
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem
quaternion_algebra.sub_self_im
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[simp]
theorem
quaternion_algebra.sub_self_re
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[protected, instance]
def
quaternion_algebra.has_mul
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
has_mul (quaternion_algebra R c₁ c₂)
Multiplication is given by
1 * x = x * 1 = x;i * i = c₁;j * j = c₂;i * j = k,j * i = -k;k * k = -c₁ * c₂;i * k = c₁ * j,k * i =-c₁ * j`;j * k = -c₂ * i, `k * j = c₂ * i`.
Equations
- quaternion_algebra.has_mul = {mul := λ (a b : quaternion_algebra R c₁ c₂), {re := a.re * b.re + c₁ * a.im_i * b.im_i + c₂ * a.im_j * b.im_j - c₁ * c₂ * a.im_k * b.im_k, im_i := a.re * b.im_i + a.im_i * b.re - c₂ * a.im_j * b.im_k + c₂ * a.im_k * b.im_j, im_j := a.re * b.im_j + c₁ * a.im_i * b.im_k + a.im_j * b.re - c₁ * a.im_k * b.im_i, im_k := a.re * b.im_k + a.im_i * b.im_j - a.im_j * b.im_i + a.im_k * b.re}}
@[simp]
theorem
quaternion_algebra.mk_mul_mk
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) :
{re := a₁, im_i := a₂, im_j := a₃, im_k := a₄} * {re := b₁, im_i := b₂, im_j := b₃, im_k := b₄} = {re := a₁ * b₁ + c₁ * a₂ * b₂ + c₂ * a₃ * b₃ - c₁ * c₂ * a₄ * b₄, im_i := a₁ * b₂ + a₂ * b₁ - c₂ * a₃ * b₄ + c₂ * a₄ * b₃, im_j := a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ - c₁ * a₄ * b₂, im_k := a₁ * b₄ + a₂ * b₃ - a₃ * b₂ + a₄ * b₁}
@[protected, nolint, instance]
def
quaternion_algebra.has_smul
{S : Type u_1}
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
[has_smul S R] :
has_smul S (quaternion_algebra R c₁ c₂)
@[protected, instance]
def
quaternion_algebra.is_scalar_tower
{S : Type u_1}
{T : Type u_2}
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
[has_smul S R]
[has_smul T R]
[has_smul S T]
[is_scalar_tower S T R] :
is_scalar_tower S T (quaternion_algebra R c₁ c₂)
@[protected, instance]
def
quaternion_algebra.smul_comm_class
{S : Type u_1}
{T : Type u_2}
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
[has_smul S R]
[has_smul T R]
[smul_comm_class S T R] :
smul_comm_class S T (quaternion_algebra R c₁ c₂)
@[protected, instance]
def
quaternion_algebra.add_comm_group
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
add_comm_group (quaternion_algebra R c₁ c₂)
Equations
- quaternion_algebra.add_comm_group = {add := has_add.add quaternion_algebra.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := has_smul.smul quaternion_algebra.has_smul, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg quaternion_algebra.has_neg, sub := has_sub.sub quaternion_algebra.has_sub, sub_eq_add_neg := _, zsmul := has_smul.smul quaternion_algebra.has_smul, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[protected, instance]
def
quaternion_algebra.add_group_with_one
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
add_group_with_one (quaternion_algebra R c₁ c₂)
Equations
- quaternion_algebra.add_group_with_one = {int_cast := λ (n : ℤ), ↑↑n, add := add_comm_group.add quaternion_algebra.add_comm_group, add_assoc := _, zero := add_comm_group.zero quaternion_algebra.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul quaternion_algebra.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg quaternion_algebra.add_comm_group, sub := add_comm_group.sub quaternion_algebra.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul quaternion_algebra.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, nat_cast := λ (n : ℕ), ↑↑n, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}
@[protected, instance]
def
quaternion_algebra.ring
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
ring (quaternion_algebra R c₁ c₂)
Equations
- quaternion_algebra.ring = {add := has_add.add quaternion_algebra.has_add, add_assoc := _, zero := add_group_with_one.zero quaternion_algebra.add_group_with_one, zero_add := _, add_zero := _, nsmul := add_group_with_one.nsmul quaternion_algebra.add_group_with_one, nsmul_zero' := _, nsmul_succ' := _, neg := add_group_with_one.neg quaternion_algebra.add_group_with_one, sub := add_group_with_one.sub quaternion_algebra.add_group_with_one, sub_eq_add_neg := _, zsmul := add_group_with_one.zsmul quaternion_algebra.add_group_with_one, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_group_with_one.int_cast quaternion_algebra.add_group_with_one, nat_cast := add_group_with_one.nat_cast quaternion_algebra.add_group_with_one, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul quaternion_algebra.has_mul, mul_assoc := _, one_mul := _, mul_one := _, npow := npow_rec {mul := has_mul.mul quaternion_algebra.has_mul}, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[protected, instance]
def
quaternion_algebra.algebra
{S : Type u_1}
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
[comm_semiring S]
[algebra S R] :
algebra S (quaternion_algebra R c₁ c₂)
Equations
- quaternion_algebra.algebra = {to_has_smul := {smul := has_smul.smul quaternion_algebra.has_smul}, to_ring_hom := {to_fun := λ (s : S), ↑(⇑(algebra_map S R) s), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
theorem
quaternion_algebra.algebra_map_eq
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(r : R) :
⇑(algebra_map R (quaternion_algebra R c₁ c₂)) r = {re := r, im_i := 0, im_j := 0, im_k := 0}
def
quaternion_algebra.re_lm
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R) :
quaternion_algebra R c₁ c₂ →ₗ[R] R
quaternion_algebra.re as a linear_map
Equations
- quaternion_algebra.re_lm c₁ c₂ = {to_fun := quaternion_algebra.re c₂, map_add' := _, map_smul' := _}
@[simp]
theorem
quaternion_algebra.re_lm_apply
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R)
(self : quaternion_algebra R c₁ c₂) :
⇑(quaternion_algebra.re_lm c₁ c₂) self = self.re
def
quaternion_algebra.im_i_lm
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R) :
quaternion_algebra R c₁ c₂ →ₗ[R] R
quaternion_algebra.im_i as a linear_map
Equations
- quaternion_algebra.im_i_lm c₁ c₂ = {to_fun := quaternion_algebra.im_i c₂, map_add' := _, map_smul' := _}
@[simp]
theorem
quaternion_algebra.im_i_lm_apply
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R)
(self : quaternion_algebra R c₁ c₂) :
⇑(quaternion_algebra.im_i_lm c₁ c₂) self = self.im_i
@[simp]
theorem
quaternion_algebra.im_j_lm_apply
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R)
(self : quaternion_algebra R c₁ c₂) :
⇑(quaternion_algebra.im_j_lm c₁ c₂) self = self.im_j
def
quaternion_algebra.im_j_lm
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R) :
quaternion_algebra R c₁ c₂ →ₗ[R] R
quaternion_algebra.im_j as a linear_map
Equations
- quaternion_algebra.im_j_lm c₁ c₂ = {to_fun := quaternion_algebra.im_j c₂, map_add' := _, map_smul' := _}
@[simp]
theorem
quaternion_algebra.im_k_lm_apply
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R)
(self : quaternion_algebra R c₁ c₂) :
⇑(quaternion_algebra.im_k_lm c₁ c₂) self = self.im_k
def
quaternion_algebra.im_k_lm
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R) :
quaternion_algebra R c₁ c₂ →ₗ[R] R
quaternion_algebra.im_k as a linear_map
Equations
- quaternion_algebra.im_k_lm c₁ c₂ = {to_fun := quaternion_algebra.im_k c₂, map_add' := _, map_smul' := _}
def
quaternion_algebra.linear_equiv_tuple
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R) :
quaternion_algebra R c₁ c₂ ≃ₗ[R] fin 4 → R
quaternion_algebra.equiv_tuple as a linear equivalence.
Equations
- quaternion_algebra.linear_equiv_tuple c₁ c₂ = {to_fun := ⇑((quaternion_algebra.equiv_tuple c₁ c₂).symm), map_add' := _, map_smul' := _, inv_fun := ⇑(quaternion_algebra.equiv_tuple c₁ c₂), left_inv := _, right_inv := _}.symm
@[simp]
theorem
quaternion_algebra.coe_linear_equiv_tuple
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R) :
⇑(quaternion_algebra.linear_equiv_tuple c₁ c₂) = ⇑(quaternion_algebra.equiv_tuple c₁ c₂)
@[simp]
theorem
quaternion_algebra.coe_linear_equiv_tuple_symm
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R) :
⇑((quaternion_algebra.linear_equiv_tuple c₁ c₂).symm) = ⇑((quaternion_algebra.equiv_tuple c₁ c₂).symm)
noncomputable
def
quaternion_algebra.basis_one_i_j_k
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R) :
basis (fin 4) R (quaternion_algebra R c₁ c₂)
ℍ[R, c₁, c₂] has a basis over R given by 1, i, j, and k.
Equations
@[simp]
theorem
quaternion_algebra.coe_basis_one_i_j_k_repr
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R)
(q : quaternion_algebra R c₁ c₂) :
@[protected, instance]
def
quaternion_algebra.module.finite
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R) :
module.finite R (quaternion_algebra R c₁ c₂)
@[protected, instance]
def
quaternion_algebra.module.free
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R) :
module.free R (quaternion_algebra R c₁ c₂)
theorem
quaternion_algebra.rank_eq_four
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R)
[strong_rank_condition R] :
module.rank R (quaternion_algebra R c₁ c₂) = 4
theorem
quaternion_algebra.finrank_eq_four
{R : Type u_3}
[comm_ring R]
(c₁ c₂ : R)
[strong_rank_condition R] :
finite_dimensional.finrank R (quaternion_algebra R c₁ c₂) = 4
theorem
quaternion_algebra.coe_commutes
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(r : R)
(a : quaternion_algebra R c₁ c₂) :
theorem
quaternion_algebra.coe_commute
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(r : R)
(a : quaternion_algebra R c₁ c₂) :
theorem
quaternion_algebra.coe_mul_eq_smul
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(r : R)
(a : quaternion_algebra R c₁ c₂) :
theorem
quaternion_algebra.mul_coe_eq_smul
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(r : R)
(a : quaternion_algebra R c₁ c₂) :
@[simp, norm_cast]
theorem
quaternion_algebra.coe_algebra_map
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
⇑(algebra_map R (quaternion_algebra R c₁ c₂)) = coe
@[protected, instance]
def
quaternion_algebra.has_star
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
has_star (quaternion_algebra R c₁ c₂)
Quaternion conjugate.
@[simp]
theorem
quaternion_algebra.re_star
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
(has_star.star a).re = a.re
@[simp]
theorem
quaternion_algebra.im_i_star
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
(has_star.star a).im_i = -a.im_i
@[simp]
theorem
quaternion_algebra.im_j_star
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
(has_star.star a).im_j = -a.im_j
@[simp]
theorem
quaternion_algebra.im_k_star
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
(has_star.star a).im_k = -a.im_k
@[simp]
theorem
quaternion_algebra.im_star
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
(has_star.star a).im = -a.im
@[protected, instance]
def
quaternion_algebra.star_ring
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
star_ring (quaternion_algebra R c₁ c₂)
Equations
- quaternion_algebra.star_ring = {to_star_semigroup := {to_has_involutive_star := {to_has_star := quaternion_algebra.has_star c₂, star_involutive := _}, star_mul := _}, star_add := _}
theorem
quaternion_algebra.self_add_star'
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
theorem
quaternion_algebra.self_add_star
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
theorem
quaternion_algebra.star_add_self'
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
theorem
quaternion_algebra.star_add_self
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
theorem
quaternion_algebra.star_eq_two_re_sub
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[protected, instance]
def
quaternion_algebra.is_star_normal
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
@[simp, norm_cast]
theorem
quaternion_algebra.star_coe
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(x : R) :
has_star.star ↑x = ↑x
@[simp]
theorem
quaternion_algebra.star_im
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
has_star.star a.im = -a.im
@[simp]
theorem
quaternion_algebra.star_smul
{S : Type u_1}
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
[monoid S]
[distrib_mul_action S R]
(s : S)
(a : quaternion_algebra R c₁ c₂) :
has_star.star (s • a) = s • has_star.star a
theorem
quaternion_algebra.eq_re_of_eq_coe
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
{a : quaternion_algebra R c₁ c₂}
{x : R}
(h : a = ↑x) :
@[simp]
theorem
quaternion_algebra.star_eq_self
{R : Type u_3}
[comm_ring R]
[no_zero_divisors R]
[char_zero R]
{c₁ c₂ : R}
{a : quaternion_algebra R c₁ c₂} :
theorem
quaternion_algebra.star_eq_neg
{R : Type u_3}
[comm_ring R]
[no_zero_divisors R]
[char_zero R]
{c₁ c₂ : R}
{a : quaternion_algebra R c₁ c₂} :
theorem
quaternion_algebra.star_mul_eq_coe
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
has_star.star a * a = ↑((has_star.star a * a).re)
theorem
quaternion_algebra.mul_star_eq_coe
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R}
(a : quaternion_algebra R c₁ c₂) :
a * has_star.star a = ↑((a * has_star.star a).re)
def
quaternion_algebra.star_ae
{R : Type u_3}
[comm_ring R]
{c₁ c₂ : R} :
quaternion_algebra R c₁ c₂ ≃ₐ[R] (quaternion_algebra R c₁ c₂)ᵐᵒᵖ
Quaternion conjugate as an alg_equiv to the opposite ring.
Equations
- quaternion_algebra.star_ae = {to_fun := mul_opposite.op ∘ has_star.star, inv_fun := has_star.star ∘ mul_opposite.unop, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
@[simp]
Space of quaternions over a type. Implemented as a structure with four fields:
re, im_i, im_j, and im_k.
Equations
- quaternion R = quaternion_algebra R (-1) (-1)
Instances for quaternion
- quaternion.has_coe_t
- quaternion.ring
- quaternion.inhabited
- quaternion.has_smul
- quaternion.is_scalar_tower
- quaternion.smul_comm_class
- quaternion.algebra
- quaternion.star_ring
- quaternion.module.finite
- quaternion.module.free
- quaternion.nontrivial
- quaternion.no_zero_divisors
- quaternion.is_domain
- quaternion.has_inv
- quaternion.group_with_zero
- quaternion.division_ring
- quaternion.has_inner
- quaternion.normed_add_comm_group
- quaternion.inner_product_space
- quaternion.norm_one_class
- quaternion.normed_division_ring
- quaternion.normed_algebra
- quaternion.cstar_ring
- quaternion.has_coe
- quaternion.complete_space
The equivalence between the quaternions over R and R × R × R × R.
Equations
- quaternion.equiv_prod R = quaternion_algebra.equiv_prod (-1) (-1)
@[simp]
theorem
quaternion.equiv_prod_apply
(R : Type u_1)
[has_one R]
[has_neg R]
(a : quaternion_algebra R (-1) (-1)) :
The equivalence between the quaternions over R and fin 4 → R.
Equations
- quaternion.equiv_tuple R = quaternion_algebra.equiv_tuple (-1) (-1)
@[simp]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
def
quaternion.has_smul
{S : Type u_1}
{R : Type u_3}
[comm_ring R]
[has_smul S R] :
has_smul S (quaternion R)
Equations
@[protected, instance]
def
quaternion.is_scalar_tower
{S : Type u_1}
{T : Type u_2}
{R : Type u_3}
[comm_ring R]
[has_smul S T]
[has_smul S R]
[has_smul T R]
[is_scalar_tower S T R] :
is_scalar_tower S T (quaternion R)
@[protected, instance]
def
quaternion.smul_comm_class
{S : Type u_1}
{T : Type u_2}
{R : Type u_3}
[comm_ring R]
[has_smul S R]
[has_smul T R]
[smul_comm_class S T R] :
smul_comm_class S T (quaternion R)
@[protected, instance]
def
quaternion.algebra
{S : Type u_1}
{R : Type u_3}
[comm_ring R]
[comm_semiring S]
[algebra S R] :
algebra S (quaternion R)
Equations
@[protected, instance]
The imaginary part of a quaternion.
Equations
- x.im = quaternion_algebra.im x
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
quaternion.smul_im
{S : Type u_1}
{R : Type u_3}
[comm_ring R]
(a : quaternion R)
[smul_zero_class S R]
(s : S) :
@[simp]
theorem
quaternion.algebra_map_def
{R : Type u_3}
[comm_ring R] :
⇑(algebra_map R (quaternion R)) = coe
@[protected, instance]
@[protected, instance]
theorem
quaternion.rank_eq_four
{R : Type u_3}
[comm_ring R]
[strong_rank_condition R] :
module.rank R (quaternion R) = 4
theorem
quaternion.finrank_eq_four
{R : Type u_3}
[comm_ring R]
[strong_rank_condition R] :
finite_dimensional.finrank R (quaternion R) = 4
@[simp]
theorem
quaternion.star_re
{R : Type u_3}
[comm_ring R]
(a : quaternion R) :
(has_star.star a).re = a.re
@[simp]
theorem
quaternion.star_im_i
{R : Type u_3}
[comm_ring R]
(a : quaternion R) :
(has_star.star a).im_i = -a.im_i
@[simp]
theorem
quaternion.star_im_j
{R : Type u_3}
[comm_ring R]
(a : quaternion R) :
(has_star.star a).im_j = -a.im_j
@[simp]
theorem
quaternion.star_im_k
{R : Type u_3}
[comm_ring R]
(a : quaternion R) :
(has_star.star a).im_k = -a.im_k
@[simp]
theorem
quaternion.star_im
{R : Type u_3}
[comm_ring R]
(a : quaternion R) :
(has_star.star a).im = -a.im
@[simp, norm_cast]
@[simp]
theorem
quaternion.im_star
{R : Type u_3}
[comm_ring R]
(a : quaternion R) :
has_star.star a.im = -a.im
@[simp]
theorem
quaternion.star_smul
{S : Type u_1}
{R : Type u_3}
[comm_ring R]
[monoid S]
[distrib_mul_action S R]
(s : S)
(a : quaternion R) :
has_star.star (s • a) = s • has_star.star a
theorem
quaternion.eq_re_of_eq_coe
{R : Type u_3}
[comm_ring R]
{a : quaternion R}
{x : R}
(h : a = ↑x) :
@[simp]
theorem
quaternion.star_eq_self
{R : Type u_3}
[comm_ring R]
[no_zero_divisors R]
[char_zero R]
{a : quaternion R} :
@[simp]
theorem
quaternion.star_eq_neg
{R : Type u_3}
[comm_ring R]
[no_zero_divisors R]
[char_zero R]
{a : quaternion R} :
theorem
quaternion.star_mul_eq_coe
{R : Type u_3}
[comm_ring R]
(a : quaternion R) :
has_star.star a * a = ↑((has_star.star a * a).re)
theorem
quaternion.mul_star_eq_coe
{R : Type u_3}
[comm_ring R]
(a : quaternion R) :
a * has_star.star a = ↑((a * has_star.star a).re)
Quaternion conjugate as an alg_equiv to the opposite ring.
Equations
@[simp]
Square of the norm.
Equations
- quaternion.norm_sq = {to_fun := λ (a : quaternion R), (a * has_star.star a).re, map_zero' := _, map_one' := _, map_mul' := _}
theorem
quaternion.norm_sq_def
{R : Type u_3}
[comm_ring R]
(a : quaternion R) :
⇑quaternion.norm_sq a = (a * has_star.star a).re
theorem
quaternion.norm_sq_coe
{R : Type u_3}
[comm_ring R]
(x : R) :
⇑quaternion.norm_sq ↑x = x ^ 2
@[simp]
@[simp]
theorem
quaternion.self_mul_star
{R : Type u_3}
[comm_ring R]
(a : quaternion R) :
a * has_star.star a = ↑(⇑quaternion.norm_sq a)
theorem
quaternion.star_mul_self
{R : Type u_3}
[comm_ring R]
(a : quaternion R) :
has_star.star a * a = ↑(⇑quaternion.norm_sq a)
theorem
quaternion.coe_norm_sq_add
{R : Type u_3}
[comm_ring R]
(a b : quaternion R) :
↑(⇑quaternion.norm_sq (a + b)) = ↑(⇑quaternion.norm_sq a) + a * has_star.star b + b * has_star.star a + ↑(⇑quaternion.norm_sq b)
theorem
quaternion.norm_sq_smul
{R : Type u_3}
[comm_ring R]
(r : R)
(q : quaternion R) :
⇑quaternion.norm_sq (r • q) = r ^ 2 * ⇑quaternion.norm_sq q
theorem
quaternion.norm_sq_add
{R : Type u_3}
[comm_ring R]
(a b : quaternion R) :
⇑quaternion.norm_sq (a + b) = ⇑quaternion.norm_sq a + ⇑quaternion.norm_sq b + 2 * (a * has_star.star b).re
@[simp]
theorem
quaternion.norm_sq_eq_zero
{R : Type u_1}
[linear_ordered_comm_ring R]
{a : quaternion R} :
⇑quaternion.norm_sq a = 0 ↔ a = 0
theorem
quaternion.norm_sq_ne_zero
{R : Type u_1}
[linear_ordered_comm_ring R]
{a : quaternion R} :
⇑quaternion.norm_sq a ≠ 0 ↔ a ≠ 0
@[simp]
theorem
quaternion.norm_sq_nonneg
{R : Type u_1}
[linear_ordered_comm_ring R]
{a : quaternion R} :
0 ≤ ⇑quaternion.norm_sq a
@[simp]
theorem
quaternion.norm_sq_le_zero
{R : Type u_1}
[linear_ordered_comm_ring R]
{a : quaternion R} :
⇑quaternion.norm_sq a ≤ 0 ↔ a = 0
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem
quaternion.sq_eq_neg_norm_sq
{R : Type u_1}
[linear_ordered_comm_ring R]
{a : quaternion R} :
@[protected, instance]
Equations
- quaternion.has_inv = {inv := λ (a : quaternion R), (⇑quaternion.norm_sq a)⁻¹ • has_star.star a}
theorem
quaternion.has_inv_inv
{R : Type u_1}
[linear_ordered_field R]
(a : quaternion R) :
a⁻¹ = (⇑quaternion.norm_sq a)⁻¹ • has_star.star a
@[protected, instance]
Equations
- quaternion.group_with_zero = {mul := monoid_with_zero.mul (semiring.to_monoid_with_zero (quaternion R)), mul_assoc := _, one := monoid_with_zero.one (semiring.to_monoid_with_zero (quaternion R)), one_mul := _, mul_one := _, npow := monoid_with_zero.npow (semiring.to_monoid_with_zero (quaternion R)), npow_zero' := _, npow_succ' := _, zero := monoid_with_zero.zero (semiring.to_monoid_with_zero (quaternion R)), zero_mul := _, mul_zero := _, inv := has_inv.inv quaternion.has_inv, div := div_inv_monoid.div._default monoid_with_zero.mul quaternion.group_with_zero._proof_8 monoid_with_zero.one quaternion.group_with_zero._proof_9 quaternion.group_with_zero._proof_10 monoid_with_zero.npow quaternion.group_with_zero._proof_11 quaternion.group_with_zero._proof_12 has_inv.inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default monoid_with_zero.mul quaternion.group_with_zero._proof_14 monoid_with_zero.one quaternion.group_with_zero._proof_15 quaternion.group_with_zero._proof_16 monoid_with_zero.npow quaternion.group_with_zero._proof_17 quaternion.group_with_zero._proof_18 has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[protected, instance]
Equations
- quaternion.division_ring = {add := ring.add quaternion.ring, add_assoc := _, zero := group_with_zero.zero quaternion.group_with_zero, zero_add := _, add_zero := _, nsmul := ring.nsmul quaternion.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg quaternion.ring, sub := ring.sub quaternion.ring, sub_eq_add_neg := _, zsmul := ring.zsmul quaternion.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast quaternion.ring, nat_cast := ring.nat_cast quaternion.ring, one := group_with_zero.one quaternion.group_with_zero, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := group_with_zero.mul quaternion.group_with_zero, mul_assoc := _, one_mul := _, mul_one := _, npow := group_with_zero.npow quaternion.group_with_zero, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := group_with_zero.inv quaternion.group_with_zero, div := group_with_zero.div quaternion.group_with_zero, div_eq_mul_inv := _, zpow := group_with_zero.zpow quaternion.group_with_zero, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := λ (q : ℚ), ↑↑q, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := has_smul.smul quaternion.has_smul, qsmul_eq_mul' := _}
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[norm_cast]
@[simp]
@[simp]
theorem
quaternion.norm_sq_div
{R : Type u_1}
[linear_ordered_field R]
(a b : quaternion R) :
⇑quaternion.norm_sq (a / b) = ⇑quaternion.norm_sq a / ⇑quaternion.norm_sq b
@[simp]
theorem
quaternion.norm_sq_zpow
{R : Type u_1}
[linear_ordered_field R]
(a : quaternion R)
(z : ℤ) :
⇑quaternion.norm_sq (a ^ z) = ⇑quaternion.norm_sq a ^ z
@[norm_cast]
theorem
cardinal.mk_quaternion_algebra
{R : Type u_1}
(c₁ c₂ : R) :
cardinal.mk (quaternion_algebra R c₁ c₂) = cardinal.mk R ^ 4
The cardinality of a quaternion algebra, as a type.
@[simp]
theorem
cardinal.mk_quaternion_algebra_of_infinite
{R : Type u_1}
(c₁ c₂ : R)
[infinite R] :
cardinal.mk (quaternion_algebra R c₁ c₂) = cardinal.mk R
The cardinality of a quaternion algebra, as a set.
@[simp]
@[simp]
theorem
cardinal.mk_quaternion
(R : Type u_1)
[has_one R]
[has_neg R] :
cardinal.mk (quaternion R) = cardinal.mk R ^ 4
The cardinality of the quaternions, as a type.
@[simp]
theorem
cardinal.mk_quaternion_of_infinite
(R : Type u_1)
[has_one R]
[has_neg R]
[infinite R] :
cardinal.mk (quaternion R) = cardinal.mk R
@[simp]
The cardinality of the quaternions, as a set.
@[simp]
theorem
cardinal.mk_univ_quaternion_of_infinite
(R : Type u_1)
[has_one R]
[has_neg R]
[infinite R] :