commgroup

Stream: new members

[BANGJI HU]

(deleted)

[BANGJI HU]

example{G : Type*} [hg :Group G] (h:∀(x : G), x*x=1) : CommGroup G :={
   hg with
   mul_comm :=by
   intro x y

}

[BANGJI HU]

help

[Ruben Van de Velde]

What do you want help with?

[Kevin Buzzard]

What's the maths proof? Lean does not find proofs automatically, your job after intro x y is to translate a complete maths proof into lean's language.

[BANGJI HU]

import Mathlib.Tactic

import Mathlib.Algebra.Group.Basic

import Mathlib.Algebra.Group.Defs

example{G : Type*} [hg :Group G] (h:∀(x : G), x*x=1) : CommGroup G :={

   hg with

   mul_comm :=by

   intro x y

   have: x*y*x*y=1 :=by rw?

   have: x*y=(x*y)⁻¹:=by?

   have: x*y=y⁻¹*x⁻¹ ：= sorry

   have： x*y=x*y      ：=

}

[BANGJI HU]

i know the proof but dont know how to program.

[BANGJI HU]

the question is every element in G if x*x=1 then if is ablean

[Eric Wieser]

Your code above has invalid space characters in it