WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Quaternion

Revision #1520 → #2183 · back to history

modifiedQuaternion6fa58f62269e
FieldFrom #1520To #2183
mathlib.decl—Quaternion
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Quaternion
note—`Quaternion R := ℍ[R,-1,0,-1]` defines quaternions over a ring, instantiated as `ℍ[R]`.
status—formalized
modifiedZero quaterniona3b36d60a4e3
FieldFrom #1520To #2183
mathlib.decl—QuaternionAlgebra.instZero
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Quaternion
note—The `Zero ℍ[R,c₁,c₂,c₃]` instance defines `0 = ⟨0,0,0,0⟩`.
status—formalized
modifiedScalar and vector parts of a quaternionea15fb979f6d
FieldFrom #1520To #2183
mathlib.decl—QuaternionAlgebra.im
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Quaternion
note—`QuaternionAlgebra.re` (the structure projection) and `QuaternionAlgebra.im` give the scalar and vector parts, with `re_add_im : ↑a.re + a.im = a`.
status—formalized
modifiedScalar quaternionccaca97d2ed1
FieldFrom #1520To #2183
mathlib.decl—QuaternionAlgebra.eq_re_iff_mem_range_coe
mathlib.match_kind—invocation
mathlib.module—Mathlib.Algebra.Quaternion
note—There is no named `IsScalar`/`isReal` predicate, but `eq_re_iff_mem_range_coe` (and `star_eq_self`) characterize quaternions equal to their real part.
status—partial
modifiedVector quaternion83d841c7545b
FieldFrom #1520To #2183
mathlib.decl—QuaternionAlgebra.star_eq_neg
mathlib.match_kind—invocation
mathlib.module—Mathlib.Algebra.Quaternion
note—Mathlib lacks a named `IsVector` predicate, but characterizes vector quaternions via `star_eq_neg ↔ a.re = 0`.
status—partial
modifiedQuaternions as a 4-dimensional vector space8875f39fbb62
FieldFrom #1520To #2183
mathlib.decl—Quaternion.finrank_eq_four
mathlib.match_kind—generalization
mathlib.module—Mathlib.Algebra.Quaternion
note—`finrank_eq_four` and `rank_eq_four` show `Module.finrank R ℍ[R] = 4`, with explicit `basisOneIJK` basis.
status—formalized
modifiedHamilton product30cc010a21ba
FieldFrom #1520To #2183
mathlib.decl—QuaternionAlgebra.instMul
mathlib.match_kind—generalization
mathlib.module—Mathlib.Algebra.Quaternion
note—The `Mul ℍ[R,c₁,c₂,c₃]` instance encodes the Hamilton product with explicit formula (`mk_mul_mk`).
status—formalized
modifiedQuaternions form a division algebrabf2efed52bdc
FieldFrom #1520To #2183
mathlib.decl—Quaternion.instDivisionRing
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Quaternion
note—`instance instDivisionRing : DivisionRing ℍ[R]` (for linearly ordered field `R`) gives the division algebra structure; combined with `Algebra R ℍ[R]`.
status—formalized
modifiedMultiplication of basis elements by 1c434105bb852
FieldFrom #1520To #2183
mathlib.decl—QuaternionAlgebra.mk_mul_mk
mathlib.match_kind—invocation
mathlib.module—Mathlib.Algebra.Quaternion
note—Multiplication by `1` follows from the `One` and `Mul` instances and `mk_mul_mk` computes any product including those with `1`.
status—formalized
modifiedProducts of basis elements i, j, k726025d2056e
FieldFrom #1520To #2183
mathlib.decl—QuaternionAlgebra.Basis.i_mul_k
mathlib.match_kind—generalization
mathlib.module—Mathlib.Algebra.QuaternionBasis
note—The `QuaternionAlgebra.Basis` API contains the products `i_mul_k`, `k_mul_i`, `k_mul_j`, `j_mul_k`, `k_mul_k` (for the standard quaternion algebra these recover ij=k etc.).
status—formalized
modifiedCenter of a noncommutative ringcdab202859cd
FieldFrom #1520To #2183
mathlib.decl—Subring.center
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Ring.Subring.Basic
note—`Subring.center R` is the subring of elements commuting with every element of `R`.
status—formalized
modifiedCenter of the quaternion algebra18177bc35918
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—I could not locate a Mathlib theorem identifying `Subring.center ℍ[ℝ]` with the scalar quaternions.
status—not_formalized
modifiedEquation z^2 + 1 = 0 over quaternions98e379170f2a
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No theorem stating the equation `z^2+1=0` over `ℍ` has infinitely many solutions appears in Mathlib.
status—not_formalized
modifiedHamilton product expansionb5b124fa5a68
FieldFrom #1520To #2183
mathlib.decl—QuaternionAlgebra.mk_mul_mk
mathlib.match_kind—generalization
mathlib.module—Mathlib.Algebra.Quaternion
note—`mk_mul_mk` (and `re_mul`, `imI_mul`, `imJ_mul`, `imK_mul` for `Quaternion`) expands the Hamilton product componentwise.
status—formalized
modifiedScalar part and vector part3f7caa821eff
FieldFrom #1520To #2183
mathlib.decl—QuaternionAlgebra.im
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Quaternion
note—`re` (projection) and `im : ℍ[R,c₁,c₂,c₃] → ℍ[R,c₁,c₂,c₃]` define the scalar and vector parts.
status—formalized
modifiedConjugate of a quaternion9aae9fa2d4fe
FieldFrom #1520To #2183
mathlib.decl—QuaternionAlgebra.instStarQuaternionAlgebra
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Quaternion
note—Quaternion conjugation is the `Star` instance on `ℍ[R,c₁,c₂,c₃]`, with `imI_star`, `imJ_star`, `imK_star` giving the negation formulas.
status—formalized
modifiedConjugation is an involutionbc85c8dfed21
FieldFrom #1520To #2183
mathlib.decl—star_star
mathlib.match_kind—invocation
mathlib.module—Mathlib.Algebra.Star.Basic
note—Mathlib's `StarRing ℍ[R,c₁,c₂,c₃]` instance (`instStarRing`) makes conjugation an involution, so `star_star a = a`.
status—formalized
modifiedConjugate of a product reverses orderdec2db3840ad
FieldFrom #1520To #2183
mathlib.decl—star_mul
mathlib.match_kind—invocation
mathlib.module—Mathlib.Algebra.Star.Basic
note—Inherited from `StarRing ℍ[R,c₁,c₂,c₃]`: `star (a * b) = star b * star a`.
status—formalized
addedConjugation expressible via quaternion arithmetic2c6669f3cd1f
modifiedExtracting scalar and vector parts via conjugation06af08e97a5c
FieldFrom #1520To #2183
mathlib.decl—Quaternion.self_add_star
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Quaternion
note—`self_add_star : a + star a = 2 * a.re` (and `re_add_im`, `sub_re_self`) recover the scalar and vector parts via conjugation.
status—formalized
modifiedNorm of a quaternion42ef6682c446
FieldFrom #1520To #2183
mathlib.decl—Quaternion.normSq
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Quaternion
note—`normSq a = (a * star a).re`, and the `NormedAddCommGroup ℍ` instance in `Mathlib.Analysis.Quaternion` provides the norm itself.
status—formalized
addedQuaternion norm equals Euclidean norm on R^456ef0c7d3ba7
modifiedNorm scales by absolute value of real scalar3252901f8f91
FieldFrom #1520To #2183
mathlib.decl—Quaternion.instNormedAlgebra
mathlib.match_kind—invocation
mathlib.module—Mathlib.Analysis.Quaternion
note—The `NormedAlgebra ℝ ℍ` instance (and `Quaternion.norm_coe`) makes scalar multiplication norm-multiplicative: `‖r • q‖ = |r| * ‖q‖`.
status—formalized
modifiedNorm is multiplicative85d89787da50
FieldFrom #1520To #2183
mathlib.decl—Quaternion.instNormedDivisionRing
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Quaternion
note—The `NormedDivisionRing ℍ` instance bundles `norm_mul a b = ‖a‖ * ‖b‖`; `normSq` is also a `MonoidWithZeroHom`.
status—formalized
modifiedDistance between quaternions0d550a505d7e
FieldFrom #1520To #2183
mathlib.decl—Quaternion.instNormedAddCommGroup
mathlib.match_kind—invocation
mathlib.module—Mathlib.Analysis.Quaternion
note—Distance `dist a b = ‖a - b‖` follows from the `NormedAddCommGroup ℍ` instance.
status—formalized
modifiedQuaternions form a metric spaceb1c1ab86322d
FieldFrom #1520To #2183
mathlib.decl—Quaternion.instNormedAddCommGroup
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Quaternion
note—`NormedAddCommGroup ℍ` (plus `CompleteSpace ℍ`) endows quaternions with a metric/complete metric space structure.
status—formalized
modifiedUnit quaternion and versorfa791764d0f6
FieldFrom #1520To #2183
mathlib.decl—Quaternion.instNormOneClass
mathlib.match_kind—invocation
mathlib.module—Mathlib.Analysis.Quaternion
note—Unit quaternions are not a named subgroup, but can be expressed via `unitary ℍ` or `Metric.sphere (0:ℍ) 1`; no dedicated `UnitQuaternion`/`versor` declaration exists.
status—partial
modifiedPolar decomposition of nonzero quaternion494035403c8b
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no explicit theorem decomposing a nonzero quaternion uniquely as norm × unit quaternion.
status—not_formalized
modifiedReciprocal of a quaternion2bc9edb2127c
FieldFrom #1520To #2183
mathlib.decl—Quaternion.instInv
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Quaternion
note—`instInv : Inv ℍ[R]` defines `a⁻¹ = (normSq a)⁻¹ • star a` (via `instGroupWithZero`/`instDivisionRing`).
status—formalized
modifiedQuaternions form a non-commutative associative algebra8dd2e844b22d
FieldFrom #1520To #2183
mathlib.decl—QuaternionAlgebra.instAlgebra
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Quaternion
note—`Algebra R ℍ[R]` plus `Ring ℍ[R]` give the associative algebra structure; non-commutativity is implicit in the multiplication formula.
status—formalized
modifiedFrobenius theorem1fd07009a68f
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib does not contain Frobenius's classification of finite-dimensional associative real division algebras.
status—not_formalized
modifiedHurwitz's theorembe02f9e32273
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Hurwitz's classification of normed division algebras over ℝ (ℝ, ℂ, ℍ, 𝕆) is not in Mathlib.
status—not_formalized
modifiedQuaternion group Q_89ab9a89cadb5
FieldFrom #1520To #2183
mathlib.decl—QuaternionGroup
mathlib.match_kind—generalization
mathlib.module—Mathlib.GroupTheory.SpecificGroups.Quaternion
note—`QuaternionGroup n` is the generalized quaternion group of order `4n`; `QuaternionGroup 2` is Q₈.
status—formalized
modifiedQuaternions as quotient of real group ring of Q_87542229c2b31
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No isomorphism `ℝ[Q₈]/⟨1+x⟩ ≃ ℍ` appears in Mathlib.
status—not_formalized
modifiedDot product of vector quaternionse68b1ea24d2b
FieldFrom #1520To #2183
mathlib.decl—Quaternion.inner_def
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.Quaternion
note—The inner product `⟪a,b⟫ = (a * star b).re` from the `InnerProductSpace ℝ ℍ` instance specializes to the 3D dot product on vector quaternions, but there is no dedicated `dot` for them.
status—partial
modifiedCross product of vector quaternionsa857ab3b6d9b
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—`Matrix.crossProduct` exists on `Fin 3 → R` but there is no formal identification of it with the vector part of `p*q` on vector quaternions.
status—not_formalized
modifiedCommutator of vector quaternionsbcba7b735d98
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—There is no Mathlib lemma identifying `p*q - q*p` of vector quaternions with twice the cross product.
status—not_formalized
modifiedCommutativity criterion via collinearity53409bc87e7d
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no theorem characterizing commuting quaternions by collinear vector parts.
status—not_formalized
modifiedUnit quaternions identified with rotations2724c8948094
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Mathlib declaration realizes the map from unit quaternions to SO(3) rotations.
status—not_formalized
modifiedRepresentation as complex 2x2 matrices36ab1a9a5d00
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No ring homomorphism `ℍ →* Matrix (Fin 2) (Fin 2) ℂ` realizing the standard 2×2 representation is in Mathlib.
status—not_formalized
modifiedProperties of complex 2x2 representationfe158304d935
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No properties (determinant=normSq, trace=2re, etc.) of a quaternion-to-2×2-complex representation appear in Mathlib.
status—not_formalized
modifiedRepresentation as real 4x4 matrices5903bcd28a64
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No quaternion-to-4×4-real representation is defined in Mathlib.
status—not_formalized
modified48 distinct real 4x4 representationsa54a4cc595f2
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No combinatorial statement about 48 such representations is in Mathlib.
status—not_formalized
modifiedLagrange's four-square theorem9f4406accf1b
FieldFrom #1520To #2183
mathlib.decl—Nat.sum_four_squares
mathlib.match_kind—exact
mathlib.module—Mathlib.NumberTheory.SumFourSquares
note—`Nat.sum_four_squares n : ∃ a b c d, a^2 + b^2 + c^2 + d^2 = n` is Lagrange's four-square theorem.
status—formalized
modifiedQuaternions via Cayley–Dickson constructionf200a79b4469
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Cayley–Dickson construction is not in Mathlib.
status—not_formalized
modifiedSquare roots of -1 form the unit sphere1f46b4ca12af
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—I could not find a Mathlib theorem characterizing `{q : ℍ | q^2 = -1}` as the unit 2-sphere in vector quaternions.
status—not_formalized
modifiedOnly negative real quaternions have infinitely many square rootsce49bb86bf18
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No statement counting square roots of quaternions appears in Mathlib.
status—not_formalized
modifiedComplex plane embedded via square root of -1a0309d6741ac
FieldFrom #1520To #2183
mathlib.decl—Quaternion.ofComplex
mathlib.match_kind—special_case
mathlib.module—Mathlib.Analysis.Quaternion
note—`Quaternion.ofComplex : ℂ →ₐ[ℝ] ℍ` is the canonical embedding using `i`; a general statement that any square root of `-1` induces an embedding is not formalized.
status—partial
modifiedSubalgebra generated by non-real quaternion911d40ce1a1a
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No theorem identifying the subalgebra generated by a non-real quaternion with `ℂ` is in Mathlib.
status—not_formalized
modifiedCommutative subrings of the quaternion ring5694ec81139c
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No description of commutative subrings of ℍ in terms of collinear vector parts is in Mathlib.
status—not_formalized
modifiedExistence of square roots of arbitrary quaternions46d5d4f46e33
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no `∃ r, r^2 = q` statement for arbitrary quaternions.
status—not_formalized
modifiedNumber of square roots by quaternion type57df117e6fb5
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No case analysis of square-root multiplicity by quaternion type is in Mathlib.
status—not_formalized
modifiedExponential of a quaternion08de3d09cd08
FieldFrom #1520To #2183
mathlib.decl—Quaternion.exp_eq
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Algebra.QuaternionExponential
note—`NormedSpace.exp ℝ : ℍ → ℍ` is available and `Quaternion.exp_eq` gives the closed-form `exp q = exp q.re • (cos‖q.im‖ + (sin‖q.im‖/‖q.im‖) • q.im)`.
status—formalized
modifiedLogarithm of a quaternion43a15dd9591a
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—There is no `Quaternion.log` definition in Mathlib.
status—not_formalized
modifiedPolar decomposition of a quaternion952e1e28bb3e
FieldFrom #1520To #2183
mathlib.decl—Quaternion.exp_eq
mathlib.match_kind—invocation
mathlib.module—Mathlib.Analysis.Normed.Algebra.QuaternionExponential
note—The polar form `q = ‖q‖ exp(θ n̂)` is implicit via `exp_eq` plus norm/im decomposition but not stated as its own decomposition theorem.
status—partial
modifiedPolar form of a unit quaternion31cc9b7a8762
FieldFrom #1520To #2183
mathlib.decl—Quaternion.exp_of_re_eq_zero
mathlib.match_kind—invocation
mathlib.module—Mathlib.Analysis.Normed.Algebra.QuaternionExponential
note—`exp_of_re_eq_zero` gives `exp(n̂ θ) = cos θ + sin θ · n̂` for imaginary `q`, the polar form of a unit quaternion, though no `polarForm` definition is named.
status—partial
modifiedPower of a quaternion1e93d3b1ab8e
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Real (non-integer) powers of quaternions are not defined in Mathlib (only `Monoid.npow`/`zpow`).
status—not_formalized
modifiedGeodesic distance between unit quaternions3cc9ab869550
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No geodesic distance on the unit-quaternion 3-sphere is defined in the Mathlib quaternion files.
status—not_formalized
modifiedConjugation by unit quaternion as rotation529fe02b814e
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No theorem that `v ↦ q * v * q⁻¹` is a rotation of ℝ³ is in Mathlib.
status—not_formalized
modifiedUnit quaternions double cover SO(3)36d8bac1f7b6
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The double cover `Spin(3) → SO(3)` via unit quaternions is not formalized in Mathlib.
status—not_formalized
modifiedVersors' group isomorphic to SU(2)350728ab4d4f
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No isomorphism between unit quaternions and SU(2) is formalized in Mathlib.
status—not_formalized
modifiedRing of Hurwitz quaternionsf2449caf7ded
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Hurwitz integer ring is absent from Mathlib (the only `Hurwitz` hits are zeta-function lemmas).
status—not_formalized
added24 unit Hurwitz quaternions form the 24-cell0cecf37c3635
modifiedQuaternion algebra over a field3c6052824d69
FieldFrom #1520To #2183
mathlib.decl—QuaternionAlgebra
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Quaternion
note—`QuaternionAlgebra R a b c` defines the generalized quaternion algebra over any ring `R`, including any field.
status—formalized
modifiedClassification of quaternion algebras454796f70f6c
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Classification of quaternion algebras over a field as either a division algebra or `M₂(F)` is not in Mathlib.
status—not_formalized
modifiedReflection formula in Cl_{3,0}a7466dc1aa2c
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Clifford-algebra reflection identity `r' = -w r w` for `Cl₃,₀(ℝ)` is not formalized.
status—not_formalized
modifiedIsomorphism between quaternions and even Cl_{3,0}4e5ac43842ec
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No isomorphism `ℍ ≃ₐ[ℝ] CliffordAlgebra⁺ (Q₃,₀)` appears in Mathlib.
status—not_formalized
modifiedBrauer group of the reals0de941477218
FieldFrom #1520To #2183
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The `BrauerGroup` is defined in `Mathlib.Algebra.BrauerGroup.Defs`, but `Br(ℝ) ≃ ℤ/2` is not proved.
status—not_formalized
modifiedArtin–Wedderburn theorem (Wedderburn's part)acb30bff2240
FieldFrom #1520To #2183
mathlib.decl—IsSemisimpleRing.isSemisimpleRing_iff_pi_matrix_divisionRing
mathlib.match_kind—exact
mathlib.module—Mathlib.RingTheory.SimpleModule.WedderburnArtin
note—`isSemisimpleRing_iff_pi_matrix_divisionRing` (and `exists_ringEquiv_matrix_divisionRing` for simple Artinian rings) is the Artin–Wedderburn structure theorem.
status—formalized
deletedScalar quaternion (restated)46669b4a114d
deletedVector quaternion (restated)50b3667fab0b