coe_toMultiplicative

Mathlib.Algebra.Group.TypeTags.Hom

URI: https://scilib.ai/kg/mathlib#MonoidHom.coe_toMultiplicative

English

For f: α →* β, the corresponding Additive version is f followed by toMul and ofMul: toAdditive f = ofMul ∘ f ∘ toMul.

Русский

Для f: α →* β выполнено toAdditive(f) = ofMul ∘ f ∘ toMul.

LaTeX

$$$\mathrm{toAdditive}(f) = \mathrm{ofMul} \circ f \circ \mathrm{toMul}$$$

Lean4

@[simp, norm_cast]
theorem coe_toMultiplicative [MulOneClass α] [MulOneClass β] (f : α →* β) : ⇑(toAdditive f) = ofMul ∘ f ∘ toMul :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru