instNonUnitalAlgHomClassOfAlgHomClass

English

Every unital algebra homomorphism is, in particular, a nonunital algebra homomorphism since it preserves the relevant structure.

Русский

Каждый канонический алгебра-гомоморфизм является, по сути, неединичным гомоморфизмом алгебр, поскольку он сохраняет соответствующую структуру.

LaTeX

$$$f:A\\to B\\text{ с единицей } \\Rightarrow f:A\\to_{\\mathrm{NonUnital}} B\\text{ является гомоморфизмом без единицы}$$$

Lean4

instance (priority := 100) [FunLike F A B] [AlgHomClass F R A B] : NonUnitalAlgHomClass F R A B :=
  { ‹AlgHomClass F R A B› with map_smulₛₗ := map_smul }

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