Commit 2024-11-27 09:56 00200113

View on Github →

chore(GroupTheory/FreeGroup): split off Reduce.lean (#19501)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/FreeGroup/Basic.lean

deleted theorem FreeGroup.Red.enum.complete

deleted theorem FreeGroup.Red.enum.sound

deleted def FreeGroup.Red.enum

deleted theorem FreeGroup.Red.reduce_left

deleted theorem FreeGroup.Red.reduce_right

deleted theorem FreeGroup.mk_toWord

deleted def FreeGroup.norm

deleted theorem FreeGroup.norm_eq_zero

deleted theorem FreeGroup.norm_inv_eq

deleted theorem FreeGroup.norm_mk_le

deleted theorem FreeGroup.norm_mul_le

deleted theorem FreeGroup.norm_of

deleted theorem FreeGroup.norm_of_pow

deleted theorem FreeGroup.norm_one

deleted theorem FreeGroup.norm_surjective

deleted theorem FreeGroup.of_ne_one

deleted theorem FreeGroup.one_ne_of

deleted theorem FreeGroup.reduce.Step.eq

deleted def FreeGroup.reduce.churchRosser

deleted theorem FreeGroup.reduce.cons

deleted theorem FreeGroup.reduce.eq_of_red

deleted theorem FreeGroup.reduce.exact

deleted theorem FreeGroup.reduce.idem

deleted theorem FreeGroup.reduce.min

deleted theorem FreeGroup.reduce.not

deleted theorem FreeGroup.reduce.red

deleted theorem FreeGroup.reduce.rev

deleted theorem FreeGroup.reduce.self

deleted theorem FreeGroup.reduce.sound

deleted def FreeGroup.reduce

deleted theorem FreeGroup.reduce_invRev

deleted theorem FreeGroup.reduce_nil

deleted theorem FreeGroup.reduce_replicate

deleted theorem FreeGroup.reduce_singleton

deleted theorem FreeGroup.reduce_toWord

deleted def FreeGroup.toWord

deleted theorem FreeGroup.toWord_eq_nil_iff

deleted theorem FreeGroup.toWord_inj

deleted theorem FreeGroup.toWord_injective

deleted theorem FreeGroup.toWord_inv

deleted theorem FreeGroup.toWord_mk

deleted theorem FreeGroup.toWord_mul_sublist

deleted theorem FreeGroup.toWord_of

deleted theorem FreeGroup.toWord_of_pow

deleted theorem FreeGroup.toWord_one

Created Mathlib/GroupTheory/FreeGroup/Reduce.lean

added theorem FreeGroup.Red.enum.complete

added theorem FreeGroup.Red.enum.sound

added def FreeGroup.Red.enum

added theorem FreeGroup.Red.reduce_left

added theorem FreeGroup.Red.reduce_right

added theorem FreeGroup.mk_toWord

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_of

added theorem FreeGroup.norm_of_pow

added theorem FreeGroup.norm_one

added theorem FreeGroup.norm_surjective

added theorem FreeGroup.of_ne_one

added theorem FreeGroup.one_ne_of

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_nil

added theorem FreeGroup.reduce_replicate

added theorem FreeGroup.reduce_singleton

added theorem FreeGroup.reduce_toWord

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_mul_sublist

added theorem FreeGroup.toWord_of

added theorem FreeGroup.toWord_of_pow

added theorem FreeGroup.toWord_one

Modified Mathlib/SetTheory/Cardinal/Free.lean