instNonUnitalAlgHomClass — Mathlib

English

Elements of the character space are non-unital algebra homomorphisms.

Русский

Элементы пространства характеристик являются ненулевыми алгомоморфизмами (ненулеподобными без единицы).

LaTeX

$$$\\text{NonUnitalAlgHomClass } (characterSpace 𝕜 A).Elem 𝕜 A 𝕜$$$

Lean4

/-- Elements of the character space are non-unital algebra homomorphisms. -/
instance instNonUnitalAlgHomClass : NonUnitalAlgHomClass (characterSpace 𝕜 A) 𝕜 A 𝕜 :=
  {
    CharacterSpace.instContinuousLinearMapClass with
    map_smulₛₗ := fun φ => map_smul φ
    map_zero := fun φ => map_zero φ
    map_mul := fun φ => φ.prop.2 }

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