linearEquivTuple — Mathlib

English

In the quaternion algebra, multiplication by the zero quaternion yields the zero quaternion: h·0 = 0 for all h, and 0·h = 0 for all h.

Русский

В кватернионной алгебре умножение на нуль даёт нуль: h·0 = 0 и 0·h = 0 для всякого h.

LaTeX

$$$h \cdot 0 = 0\quad\text{and}\quad 0 \cdot h = 0\ \text{for all } h \in \mathbb{H}(R;c_1,c_2,c_3).$$$

Lean4

/-- `QuaternionAlgebra.equivTuple` as a linear equivalence. -/
def linearEquivTuple : ℍ[R,c₁,c₂,c₃] ≃ₗ[R] Fin 4 → R :=
  LinearEquiv.symm
    { (equivTuple c₁ c₂ c₃).symm with
      toFun := (equivTuple c₁ c₂ c₃).symm
      invFun := equivTuple c₁ c₂ c₃
      map_add' := fun _ _ => rfl
      map_smul' := fun _ _ => rfl }

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