Set_of_all_Self_Maps_is_Monoid
Provedmapping-theorymonoidsproofwiki
The set of all mappings from S to itself under composition forms a monoid whose identity is the identity mapping.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Set_of_all_Self_Maps_is_Monoid (S : Type _) : ∀ (f : S → S), Function.comp id f = f := by sorry
Source