isLocalHom_toMonoidHom — Mathlib

English

If f is a local homomorphism as a function between FunLike structures, then the induced MonoidHom structure f : R →* S is also local.

Русский

Если f — локальный гомоморфизм как функция между FunLike структурами, то получаемая MonoidHom структура f : R →* S тоже локальна.

LaTeX

$$$[IsLocalHom f] \\Rightarrow IsLocalHom (f : R \\to* S)$$$

Lean4

@[instance 100]
theorem isLocalHom_toMonoidHom (f : F) [IsLocalHom f] : IsLocalHom (f : R →* S) :=
  ⟨IsLocalHom.map_nonunit (f := f)⟩

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