instNonUnitalAlgSemiHomClass — Mathlib

English

The collection of nonunital algebra homomorphisms forms a NonUnitalAlgSemiHomClass, i.e., a structure that respects addition, zero, multiplication, and scalar action.

Русский

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

LaTeX

$$$\text{NonUnitalAlgSemiHomClass } (A \to_{\varphi} B) \; A \; B$$$

Lean4

instance : NonUnitalAlgSemiHomClass (A →ₛₙₐ[φ] B) φ A B
    where
  map_add f := f.map_add'
  map_zero f := f.map_zero'
  map_mul f := f.map_mul'
  map_smulₛₗ f := f.map_smul'

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