toNonUnitalAlgHom — Mathlib

English

From a character, one obtains a non-unital algebra homomorphism A →𝕜.

Русский

Из элемента пространства характеристик получается ненулевой алгоморфизм $A \\to 𝕜$ без единицы.

LaTeX

$$$\\text{toNonUnitalAlgHom }(φ) : A \\toₙₐ[𝕜] 𝕜$$$

Lean4

/-- An element of the character space, as a non-unital algebra homomorphism. -/
def toNonUnitalAlgHom (φ : characterSpace 𝕜 A) : A →ₙₐ[𝕜] 𝕜
    where
  toFun := (φ : A → 𝕜)
  map_mul' := map_mul φ
  map_smul' := map_smul φ
  map_zero' := map_zero φ
  map_add' := map_add φ

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