imIₗ — Mathlib

English

The real part projection re defines an R-linear map from the quaternion algebra to R: reₗ ∈ Hom_R(ℍ[R,c1,c2,c3], R).

Русский

Проекция вещественной части re задаёт линейное по модулю R отображение из кватернионной алгебры в R: reₗ ∈ Hom_R(ℍ[R,c1,c2,c3], R).

LaTeX

$$$re_{\ell} \in \operatorname{Hom}_R\big(\mathbb{H}(R;c_1,c_2,c_3), R\big).$$$

Lean4

/-- `QuaternionAlgebra.imI` as a `LinearMap` -/
@[simps]
def imIₗ : ℍ[R,c₁,c₂,c₃] →ₗ[R] R where
  toFun := imI
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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