toMonoidWithZeroHomClass — Mathlib

English

From a MulEquivClass, derive a MonoidWithZeroHomClass when available.

Русский

Из класса эквивалентностей по умножению выводят класс гомоморфизмов, сохраняющих нуль, при наличии условий.

LaTeX

$$$\\text{MulEquivClass} \\Rightarrow \\text{MonoidWithZeroHomClass}$$$

Lean4

instance (priority := 100) toMonoidWithZeroHomClass [MulZeroOneClass α] [MulZeroOneClass β] [MulEquivClass F α β] :
    MonoidWithZeroHomClass F α β :=
  { MulEquivClass.instMonoidHomClass F, MulEquivClass.toZeroHomClass with }

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