coe_basisOneIJK_repr — Mathlib

English

For any quaternion q, the repr under basisOneIJK is the vector of its components [q.re, q.imI, q.imJ, q.imK].

Русский

Для кватерниона q представление по базису basisOneIJK дает вектор [q.re, q.imI, q.imJ, q.imK].

LaTeX

$$$\bigl(basisOneIJK\, c_1\, c_2\, c_3\bigr).repr(q) = \langle q.re, q.imI, q.imJ, q.imK \rangle.$$$

Lean4

@[simp]
theorem coe_basisOneIJK_repr (q : ℍ[R,c₁,c₂,c₃]) : ((basisOneIJK c₁ c₂ c₃).repr q) = ![q.re, q.imI, q.imJ, q.imK] :=
  rfl

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