coe_mk — Mathlib

English

If f: A →* B is a monoid homomorphism and h is a witness that f preserves the star operation, then the star-monoid homomorphism ⟨f, h⟩ has underlying map f.

Русский

Пусть f: A →* B — моноидный гомоморфизм и есть доказательство того, что f сохраняет операцию звезды. Тогда звездный моноидный гомоморфизм ⟨f, h⟩ имеет подлежащую карту f.

LaTeX

$$$\\bigl(\\langle f, h \\rangle : A \\to⋆* B\\bigr) : A \\to B = f$$$

Lean4

@[simp]
theorem coe_mk (f : A →* B) (h) : ((⟨f, h⟩ : A →⋆* B) : A → B) = f :=
  rfl

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