id — Mathlib · SciLib

English

If f: A →* B is a monoid homomorphism and h is a witness that f preserves star, 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

/-- The identity as a star monoid homomorphism. -/
protected def id : A →⋆* A :=
  { (.id A : A →* A) with map_star' := fun _ ↦ rfl }

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