coe_comp_mulHom

Mathlib.Algebra.Ring.Hom.Defs

URI: https://scilib.ai/kg/mathlib#NonUnitalRingHom.coe_comp_mulHom

Lean4

@[simp]
theorem coe_comp_mulHom (g : β →ₙ+* γ) (f : α →ₙ+* β) : MulHom.mk (g ∘ f) (g.comp f).map_mul' = (g : β →ₙ* γ).comp f :=
  rfl

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

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

Разделы

Аффилиация

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