toAddMonoidHomClass — Mathlib

English

The NormedAddGroupHom V1 V2 inherits an AddMonoidHomClass structure, mapping addition and zero compatibly.

Русский

NormedAddGroupHom V1 V2 наследует структуру AddMonoidHomClass, сохраняющую сложение и ноль.

LaTeX

$$$\\text{instance } toAddMonoidHomClass : AddMonoidHomClass (NormedAddGroupHom V_1 V_2) V_1 V_2$$$

Lean4

instance toAddMonoidHomClass : AddMonoidHomClass (NormedAddGroupHom V₁ V₂) V₁ V₂
    where
  map_add f := f.map_add'
  map_zero f := (AddMonoidHom.mk' f.toFun f.map_add').map_zero

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