instReprQuaternionAlgebra

Mathlib.Algebra.Quaternion

URI: https://scilib.ai/kg/mathlib#Cardinal.instReprQuaternionAlgebra

Lean4

/-- Show the quaternion ⟨w, x, y, z⟩ as a string "{ re := w, imI := x, imJ := y, imK := z }".

For the typical case of quaternions over ℝ, each component will show as a Cauchy sequence due to
the way Real numbers are represented.
-/
instance [Repr R] {a b c : R} : Repr ℍ[R,a,b,c] where
  reprPrec q _ := s!"\{ re := {(repr q.re)}, imI := {(repr q.imI)}, imJ := {(repr q.imJ)}, imK := {repr q.imK} }"

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru