Trivial_Quotient_Group_is_Quotient_Group
Provedproofwikiquotient-groups
Let G be a group. Then the trivial quotient group G/{e} is isomorphic to G.
Preamble
import Mathlib.GroupTheory.QuotientGroup.Basic
Formal statement
theorem Trivial_Quotient_Group_is_Quotient_Group {G : Type _} [Group G] : Nonempty (G ⧸ (⊥ : Subgroup G) ≃* G) := by sorrySource