coe_toAdditiveLeft — Mathlib

English

The coercion to AddMonoidHom from MonoidHom toAdditiveLeft is given by composition with toAdd and toMul.

Русский

Коэрция к AddMonoidHom из MonoidHom toAdditiveLeft задаётся композицией с toAdd и toMul.

LaTeX

$$$\text{coe_toAdditiveLeft} = \text{comp}_{toAdd, toMul}$$$

Lean4

@[simp, norm_cast]
theorem coe_toAdditiveLeft [MulOneClass α] [AddZeroClass β] (f : α →* Multiplicative β) :
    ⇑(toAdditiveLeft f) = toAdd ∘ f ∘ toMul :=
  rfl

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