coe_toAdditiveRight — Mathlib

English

For AddZeroClass α and MulOneClass β and any f: Multiplicative α →* β, the underlying function of the additive reinterpretation equals the composition of the standard coercions with f.

Русский

Для AddZeroClass α и MulOneClass β и любого f: Multiplicative α →* β, базовая функция аддитивного преобразования равна композиции обычных отображений с f.

LaTeX

$$$\\bigl(\\text{toAdditiveRight } f\\bigr) = \\operatorname{ofMul} \\circ f \\circ \\operatorname{ofAdd}$$$

Lean4

@[simp, norm_cast]
theorem coe_toAdditiveRight [AddZeroClass α] [MulOneClass β] (f : Multiplicative α →* β) :
    ⇑(toAdditiveRight f) = ofMul ∘ f ∘ ofAdd :=
  rfl

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