mk_toAddMonoidHom — Mathlib

English

The AddMonoidHom obtained from the triple (f,h1) matches the canonical constructor: f is mapped to AddMonoidHom.mk' f h1.

Русский

Аддинг-монойд-гомоморфизм, полученный из тройки (f,h1), совпадает с каноническим конструктором: AddMonoidHom.mk' f h1.

LaTeX

$$$ (\\langle f,h_1,h_2\\rangle : NormedAddGroupHom\\ V_1\\ V_2).toAddMonoidHom = AddMonoidHom.mk' f h_1 $$$

Lean4

@[simp]
theorem mk_toAddMonoidHom (f) (h₁) (h₂) :
    (⟨f, h₁, h₂⟩ : NormedAddGroupHom V₁ V₂).toAddMonoidHom = AddMonoidHom.mk' f h₁ :=
  rfl

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