imJₗ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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