Identity_Mapping_is_Left_Identity
Provedidentity-mappingsproofwiki
Let f: S → T be a mapping. Then I_T ∘ f = f, where I_T is the identity mapping on T.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Identity_Mapping_is_Left_Identity {α β : Type _} (f : α → β) : id ∘ f = f := by sorrySource