toMonoidHom_mapEquiv — Mathlib

English

The toMonoidHom component of mapEquiv coincides with the map induced by the underlying equivalence on monoids.

Русский

Компоненту toMonoidHom отображения mapEquiv соответствует отображение между моноидами, индуцированное соответствием.

LaTeX

$$$ (mapEquiv f).toStarMonoidHom = map f.toStarMonoidHom $$$

Lean4

@[simp]
theorem toMonoidHom_mapEquiv (f : R ≃⋆* S) : (mapEquiv f).toStarMonoidHom = map f.toStarMonoidHom :=
  rfl

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