Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-22 11:11 00eb6910

View on Github →

feat(group_theory/free_group): norm of elements (#15503) This PR adds to a new free_group.metric namespace some useful lemmas related to the word metric on the free group. This will be useful for defining the word metric for an arbitrary (marked) group.

Estimated changes

Modified src/group_theory/free_group.lean

modified theorem free_group.inv_mk

added def free_group.inv_rev

added theorem free_group.inv_rev_bijective

added theorem free_group.inv_rev_empty

added theorem free_group.inv_rev_injective

added theorem free_group.inv_rev_inv_rev

added theorem free_group.inv_rev_involutive

added theorem free_group.inv_rev_length

added theorem free_group.inv_rev_surjective

added theorem free_group.mk_to_word

added def free_group.norm

added theorem free_group.norm_eq_zero

added theorem free_group.norm_inv_eq

added theorem free_group.norm_mk_le

added theorem free_group.norm_mul_le

added theorem free_group.norm_one

modified theorem free_group.red.antisymm

added theorem free_group.red.inv_rev

added theorem free_group.red.length_le

added theorem free_group.red.reduce_left

added theorem free_group.red.reduce_right

added theorem free_group.red.step.inv_rev

added theorem free_group.red.step_inv_rev_iff

deleted theorem free_group.red.sublist

added theorem free_group.red_inv_rev_iff

modified theorem free_group.reduce.idem

added theorem free_group.reduce_inv_rev

added theorem free_group.reduce_to_word

deleted theorem free_group.to_word.inj

deleted theorem free_group.to_word.mk

added theorem free_group.to_word_eq_nil_iff

added theorem free_group.to_word_inj

added theorem free_group.to_word_injective

added theorem free_group.to_word_inv

added theorem free_group.to_word_mk

added theorem free_group.to_word_one