imKₗ — Mathlib

English

The k-coordinate projection imK defines an R-linear map: imKₗ ∈ Hom_R(ℍ[R,c1,c2,c3], R).

Русский

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

LaTeX

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

Lean4

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

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