Identity_Mapping_is_Automorphism
Provedautomorphismsidentity-mappingsproofwiki
The identity mapping on an algebraic structure is an automorphism.
Preamble
import Mathlib.Algebra.Group.Equiv.Basic
Formal statement
theorem Identity_Mapping_is_Automorphism {G : Type _} [Group G] : (MulEquiv.refl G).toMonoidHom = MonoidHom.id G := by sorrySource