coeOutMonoidHom — Mathlib

English

There is a canonical CoeOut from AlgHom to MonoidHom, i.e., an algebra homomorphism can be viewed as a multiplicative monoid homomorphism.

Русский

Существует каноническое отображение CoeOut от AlgHom к MonoidHom, то есть алгоморфизм можно рассматривать как моноид-гомоморфизм умножения.

LaTeX

$$$\\text{AlgHom} \\to \\text{MonoidHom}$$$

Lean4

instance coeOutMonoidHom : CoeOut (A →ₐ[R] B) (A →* B) :=
  ⟨AlgHom.toMonoidHom'⟩

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