Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-25 14:28 716decc0

View on Github →

feat(algebra): add free groups (#89)

Estimated changes

Created algebra/free_group.lean

added theorem free_group.church_rosser

added theorem free_group.church_rosser_1

added def free_group.free_group_congr

added def free_group.free_group_empty_equiv_unit

added def free_group.free_group_unit_equiv_int

added def free_group.inv

added def free_group.map.aux

added theorem free_group.map.comp

added theorem free_group.map.id'

added theorem free_group.map.id

added theorem free_group.map.inv

added theorem free_group.map.mk

added theorem free_group.map.mul

added theorem free_group.map.of

added theorem free_group.map.one

added theorem free_group.map.unique

added def free_group.map

added theorem free_group.map_eq_to_group

added def free_group.mk

added theorem free_group.mul_mk

added theorem free_group.of.inj

added def free_group.of

added theorem free_group.prod.inv

added theorem free_group.prod.mul

added theorem free_group.prod.of

added theorem free_group.prod.one

added theorem free_group.prod.unique

added def free_group.prod

added theorem free_group.prod_mk

added theorem free_group.quot_lift_mk

added theorem free_group.quot_lift_on_mk

added theorem free_group.quot_mk_eq_mk

added theorem free_group.red.antisymm

added theorem free_group.red.append

added theorem free_group.red.bnot

added theorem free_group.red.cons

added theorem free_group.red.cons_bnot

added theorem free_group.red.cons_bnot_rev

added theorem free_group.red.cons_iff

added theorem free_group.red.enum.complete

added theorem free_group.red.enum.sound

added def free_group.red.enum

added theorem free_group.red.inv_of_red_nil.aux

added theorem free_group.red.inv_of_red_nil

added theorem free_group.red.inv_of_red_of_ne.aux

added theorem free_group.red.inv_of_red_of_ne

added theorem free_group.red.length

added theorem free_group.red.nil.aux

added theorem free_group.red.nil

added theorem free_group.red.of_cons

added theorem free_group.red.of_step

added theorem free_group.red.singleton.aux

added theorem free_group.red.singleton

added theorem free_group.red.sizeof

added theorem free_group.red.step.append_left

added theorem free_group.red.step.append_right

added theorem free_group.red.step.bnot_rev

added theorem free_group.red.step.church_rosser.aux2

added theorem free_group.red.step.church_rosser.aux

added theorem free_group.red.step.church_rosser

added theorem free_group.red.step.cons

added theorem free_group.red.step.cons_bnot

added theorem free_group.red.step.eqv_gen_of_red

added theorem free_group.red.step.exact

added theorem free_group.red.step.inv

added theorem free_group.red.step.length

added theorem free_group.red.step.sound

added theorem free_group.red.step.sublist

added theorem free_group.red.step.to_group

added inductive free_group.red.step

added theorem free_group.red.sublist

added theorem free_group.red.to_group

added theorem free_group.red.trans.aux

added theorem free_group.red.trans

added inductive free_group.red

added def free_group.reduce.church_rosser

added theorem free_group.reduce.cons

added theorem free_group.reduce.eq_of_red

added theorem free_group.reduce.exact

added theorem free_group.reduce.idem

added theorem free_group.reduce.min

added theorem free_group.reduce.not

added theorem free_group.reduce.red

added theorem free_group.reduce.rev

added theorem free_group.reduce.self

added theorem free_group.reduce.sound

added theorem free_group.reduce.step.eq

added def free_group.reduce

added theorem free_group.sum.inv

added theorem free_group.sum.of

added theorem free_group.sum.one

added theorem free_group.sum.sum

added def free_group.sum

added theorem free_group.sum_mk

added def free_group.to_group.aux

added theorem free_group.to_group.inv

added theorem free_group.to_group.mk

added theorem free_group.to_group.mul

added theorem free_group.to_group.of

added theorem free_group.to_group.of_eq

added theorem free_group.to_group.one

added theorem free_group.to_group.range_eq_closure

added theorem free_group.to_group.range_subset

added theorem free_group.to_group.unique

added def free_group.to_group

added theorem free_group.to_group_eq_prod_map

added def free_group.to_word.inj

added def free_group.to_word.mk

added def free_group.to_word

added def free_group

added theorem list.append_eq_has_append

added theorem list.infix_cons

Modified group_theory/subgroup.lean