comp — Mathlib

English

The composition of star-monoid morphisms f: B →⋆* C and g: A →⋆* B is a star-monoid morphism A →⋆* C, and its action on an element a ∈ A is the successive application: f(g(a)).

Русский

Сложение звездно-монойдных отображений f: B →⋆* C и g: A →⋆* B образует звездный моноидный гомоморфизм A →⋆* C, а его значение на элементе a ∈ A равно f(g(a)).

LaTeX

$$$ (comp\\ f\\ g)(a) = f(g(a)) $$$

Lean4

/-- The composition of star monoid homomorphisms, as a star monoid homomorphism. -/
def comp (f : B →⋆* C) (g : A →⋆* B) : A →⋆* C :=
  { f.toMonoidHom.comp g.toMonoidHom with map_star' := fun a => by simp [map_star] }

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