Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-26 18:29 48485a2e

View on Github →

refactor(logic/relation,group_theory/free_group): add theory for reflextive/transitive relations & use them for the free group reduction

Estimated changes

added theorem list.infix_cons
added theorem list.nil_eq_append_iff
deleted theorem free_group.church_rosser
deleted def free_group.inv
added theorem free_group.inv_mk
modified theorem free_group.map.comp
added theorem free_group.one_eq_mk
modified theorem free_group.red.antisymm
deleted theorem free_group.red.append
deleted theorem free_group.red.bnot
deleted theorem free_group.red.cons
deleted theorem free_group.red.cons_bnot
deleted theorem free_group.red.cons_iff
added theorem free_group.red.exact
modified theorem free_group.red.length
deleted theorem free_group.red.nil.aux
deleted theorem free_group.red.nil
added theorem free_group.red.nil_iff
deleted theorem free_group.red.of_cons
deleted theorem free_group.red.of_step
added theorem free_group.red.refl
deleted theorem free_group.red.singleton
deleted theorem free_group.red.sizeof
modified theorem free_group.red.step.cons
deleted theorem free_group.red.step.exact
deleted theorem free_group.red.step.inv
modified theorem free_group.red.step.length
deleted theorem free_group.red.step.sound
modified theorem free_group.red.step.sublist
modified theorem free_group.red.sublist
deleted theorem free_group.red.to_group
deleted theorem free_group.red.trans.aux
modified theorem free_group.red.trans
added def free_group.red
deleted inductive free_group.red
modified theorem free_group.reduce.not
modified def free_group
deleted theorem list.append_eq_has_append
deleted theorem list.infix_cons
added theorem relation.church_rosser
added theorem relation.eqv_gen_mono
added def relation.join
added inductive relation.refl_gen
added inductive relation.refl_trans_gen