Commit 2021-09-14 12:09 2a3cd41b

View on Github →

feat(group_theory/free_product): equivalence with reduced words (#7395) We show that each element of the free product is represented by a unique reduced word.

Estimated changes

Modified src/group_theory/free_product.lean

added theorem free_product.word.cons_eq_rcons

added theorem free_product.word.cons_eq_smul

added def free_product.word.empty

added def free_product.word.equiv

added def free_product.word.equiv_pair

added theorem free_product.word.equiv_pair_eq_of_fst_idx_ne

added theorem free_product.word.equiv_pair_symm

added def free_product.word.fst_idx

added theorem free_product.word.fst_idx_ne_iff

added theorem free_product.word.of_smul_def

added structure free_product.word.pair

added def free_product.word.prod

added theorem free_product.word.prod_nil

added theorem free_product.word.prod_rcons

added theorem free_product.word.prod_smul

added def free_product.word.rcons

added theorem free_product.word.rcons_inj

added theorem free_product.word.smul_induction

added structure free_product.word