endomorphism of a finite group G

Stream: new members

[BANGJI HU]

suppose that f:G \to G is a endomorphism of a finite group G then f is automorphism iff f is injective

[BANGJI HU]

suppose that f:G \to G is a endomorphism of a finite group G then f is automorphism iff f is injective

[BANGJI HU]

import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Defs
import Mathlib.GroupTheory.OrderOfElement


import Mathlib.GroupTheory.GroupAction.Group
import Mathlib.GroupTheory.GroupAction.Hom



variables {G : Type*} [fintype G] [group G]


variables (f : G →* G)


lemma endomorphism_injective_iff_bijective : function.injective f ↔ function.bijective f :=

    construction
    intro hf,

    exact fintype.injective_iff_bijectivef
    intro hf,
    exact hf

theorem endomorphism_iff_isomorphism : function.injective f ↔ is_group_hom f ∧ function.bijective f :=

    construction
    intro hf,
      exact f.is_group_hom
      exact endomorphism_injective_iff_bijective f hf
    intro h,
    exact h

[BANGJI HU]

my question is i know the proof but how can i translate to lean

[Daniel Weber]

Are you working in Lean 3?

[Ruben Van de Velde]

Clearly no, but also clearly not lean 4. What did you look at to get to this point?

[Kevin Buzzard]

A language model?