equivTuple_apply — Mathlib

English

The equivalence sends a quaternion to its four coordinates (re, imI, imJ, imK).

Русский

Это изоморфизм отправляет кватернион в его четыре координаты (re, imI, imJ, imK).

LaTeX

$$$\text{equivTuple}_{R}(c_1,c_2,c_3)(x) = (x.re, x.imI, x.imJ, x.imK).$$$

Lean4

@[simp]
theorem equivTuple_apply {R : Type*} (c₁ c₂ c₃ : R) (x : ℍ[R,c₁,c₂,c₃]) :
    equivTuple c₁ c₂ c₃ x = ![x.re, x.imI, x.imJ, x.imK] :=
  rfl

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