coe_toMultiplicative — Mathlib

English

For any AddMonoidHom f, the underlying function of its multiplicative version equals the composition of toAdd, f, and ofAdd: coe(toMultiplicative f) = ofAdd ∘ f ∘ toAdd.

Русский

Для любого отображения AddMonoidHom f базовая функция его мультипликативной версии равна композиции toAdd, f и ofAdd: coe(toMultiplicative f) = ofAdd ∘ f ∘ toAdd.

LaTeX

$$toMultiplicative f = ofAdd ∘ f ∘ toAdd$$

Lean4

@[simp, norm_cast]
theorem coe_toMultiplicative [AddZeroClass α] [AddZeroClass β] (f : α →+ β) :
    ⇑(toMultiplicative f) = ofAdd ∘ f ∘ toAdd :=
  rfl

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