Commit 2023-01-27 13:56 ec0f1c60

View on Github →

feat: port GroupTheory.FreeGroup (#1867)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/FreeGroup.lean

added inductive FreeAddGroup.Red.Step

added def FreeGroup.Lift.aux

added theorem FreeGroup.Red.Step.append_left

added theorem FreeGroup.Red.Step.append_left_iff

added theorem FreeGroup.Red.Step.append_right

added theorem FreeGroup.Red.Step.cons

added theorem FreeGroup.Red.Step.cons_cons_iff

added theorem FreeGroup.Red.Step.cons_left_iff

added theorem FreeGroup.Red.Step.cons_not

added theorem FreeGroup.Red.Step.cons_not_rev

added theorem FreeGroup.Red.Step.diamond

added theorem FreeGroup.Red.Step.diamond_aux

added theorem FreeGroup.Red.Step.invRev

added theorem FreeGroup.Red.Step.length

added theorem FreeGroup.Red.Step.lift

added theorem FreeGroup.Red.Step.not_rev

added theorem FreeGroup.Red.Step.sublist

added theorem FreeGroup.Red.Step.to_red

added inductive FreeGroup.Red.Step

added theorem FreeGroup.Red.antisymm

added theorem FreeGroup.Red.append_append

added theorem FreeGroup.Red.append_append_left_iff

added theorem FreeGroup.Red.church_rosser

added theorem FreeGroup.Red.cons_cons

added theorem FreeGroup.Red.cons_cons_iff

added theorem FreeGroup.Red.cons_nil_iff_singleton

added theorem FreeGroup.Red.enum.complete

added theorem FreeGroup.Red.enum.sound

added def FreeGroup.Red.enum

added theorem FreeGroup.Red.exact

added theorem FreeGroup.Red.invRev

added theorem FreeGroup.Red.inv_of_red_of_ne

added theorem FreeGroup.Red.length

added theorem FreeGroup.Red.length_le

added theorem FreeGroup.Red.nil_iff

added theorem FreeGroup.Red.not_step_nil

added theorem FreeGroup.Red.not_step_singleton

added theorem FreeGroup.Red.red_iff_irreducible

added theorem FreeGroup.Red.reduce_left

added theorem FreeGroup.Red.reduce_right

added theorem FreeGroup.Red.refl

added theorem FreeGroup.Red.singleton_iff

added theorem FreeGroup.Red.sizeof_of_step

added theorem FreeGroup.Red.step_invRev_iff

added theorem FreeGroup.Red.to_append_iff

added theorem FreeGroup.Red.trans

added def FreeGroup.Red

added theorem FreeGroup.equivalence_join_red

added theorem FreeGroup.eqvGen_step_iff_join_red

added theorem FreeGroup.ext_hom

added def FreeGroup.freeGroupCongr

added theorem FreeGroup.freeGroupCongr_refl

added theorem FreeGroup.freeGroupCongr_symm

added theorem FreeGroup.freeGroupCongr_trans

added def FreeGroup.freeGroupEmptyEquivUnit

added def FreeGroup.freeGroupUnitEquivInt

added def FreeGroup.invRev

added theorem FreeGroup.invRev_bijective

added theorem FreeGroup.invRev_empty

added theorem FreeGroup.invRev_injective

added theorem FreeGroup.invRev_invRev

added theorem FreeGroup.invRev_involutive

added theorem FreeGroup.invRev_length

added theorem FreeGroup.invRev_surjective

added theorem FreeGroup.inv_bind

added theorem FreeGroup.inv_mk

added theorem FreeGroup.join_red_of_step

added theorem FreeGroup.lift.mk

added theorem FreeGroup.lift.of

added theorem FreeGroup.lift.of_eq

added theorem FreeGroup.lift.range_eq_closure

added theorem FreeGroup.lift.range_le

added theorem FreeGroup.lift.unique

added def FreeGroup.lift

added theorem FreeGroup.lift_eq_prod_map

added theorem FreeGroup.map.comp

added theorem FreeGroup.map.id'

added theorem FreeGroup.map.id

added theorem FreeGroup.map.mk

added theorem FreeGroup.map.of

added theorem FreeGroup.map.unique

added def FreeGroup.map

added theorem FreeGroup.map_eq_lift

added theorem FreeGroup.map_inv

added theorem FreeGroup.map_mul

added theorem FreeGroup.map_one

added theorem FreeGroup.map_pure

added def FreeGroup.mk

added theorem FreeGroup.mk_toWord

added theorem FreeGroup.mul_bind

added theorem FreeGroup.mul_mk

added def FreeGroup.norm

added theorem FreeGroup.norm_eq_zero

added theorem FreeGroup.norm_inv_eq

added theorem FreeGroup.norm_mk_le

added theorem FreeGroup.norm_mul_le

added theorem FreeGroup.norm_one

added def FreeGroup.of

added theorem FreeGroup.of_injective

added theorem FreeGroup.one_bind

added theorem FreeGroup.one_eq_mk

added theorem FreeGroup.prod.of

added theorem FreeGroup.prod.unique

added def FreeGroup.prod

added theorem FreeGroup.prod_mk

added theorem FreeGroup.pure_bind

added theorem FreeGroup.quot_liftOn_mk

added theorem FreeGroup.quot_lift_mk

added theorem FreeGroup.quot_map_mk

added theorem FreeGroup.quot_mk_eq_mk

added theorem FreeGroup.red_invRev_iff

added theorem FreeGroup.reduce.Step.eq

added def FreeGroup.reduce.churchRosser

added theorem FreeGroup.reduce.cons

added theorem FreeGroup.reduce.eq_of_red

added theorem FreeGroup.reduce.exact

added theorem FreeGroup.reduce.idem

added theorem FreeGroup.reduce.min

added theorem FreeGroup.reduce.not

added theorem FreeGroup.reduce.red

added theorem FreeGroup.reduce.rev

added theorem FreeGroup.reduce.self

added theorem FreeGroup.reduce.sound

added def FreeGroup.reduce

added theorem FreeGroup.reduce_invRev

added theorem FreeGroup.reduce_toWord

added theorem FreeGroup.sum.map_inv

added theorem FreeGroup.sum.map_mul

added theorem FreeGroup.sum.map_one

added theorem FreeGroup.sum.of

added def FreeGroup.sum

added theorem FreeGroup.sum_mk

added def FreeGroup.toWord

added theorem FreeGroup.toWord_eq_nil_iff

added theorem FreeGroup.toWord_inj

added theorem FreeGroup.toWord_injective

added theorem FreeGroup.toWord_inv

added theorem FreeGroup.toWord_mk

added theorem FreeGroup.toWord_one

added def FreeGroup