instMul

Mathlib.Algebra.GroupWithZero.Hom

URI: https://scilib.ai/kg/mathlib#MonoidWithZeroHom.instMul

Lean4

/-- Given two monoid with zero morphisms `f`, `g` to a commutative monoid with zero, `f * g` is the
monoid with zero morphism sending `x` to `f x * g x`. -/
instance {β} [CommMonoidWithZero β] : Mul (α →*₀ β) where
  mul f g := { (f * g : α →* β) with map_zero' := by dsimp; rw [map_zero, zero_mul] }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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