mathlib3
2a3cd41b - feat(group_theory/free_product): equivalence with reduced words (#7395)

Commit

4 years ago

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.

Author

dwarn

Parents

7deb32cb

mathlib3 2a3cd41b - feat(group_theory/free_product): equivalence with reduced words (#7395)

mathlib3
2a3cd41b - feat(group_theory/free_product): equivalence with reduced words (#7395)