New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(group_theory/free_monoid_product): define free monoid/group product #2578
Conversation
@@ -0,0 +1,400 @@ | |||
import algebra.free_monoid group_theory.congruence tactic.simp_rw algebra.opposites |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
header
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It has a WIP label.
Some lemmas I found useful for #2578
Some lemmas I found useful for leanprover-community#2578
Some lemmas I found useful for leanprover-community#2578
By the way, I've been working on coproducts of monoids myself. I've done it differently from this, I don't use quotients and instead reduce the words when I multiply. This is obviously better for computation, but it also has some other advantages; there are some proofs about free groups that induct on the length of a word, but length does not make sense without reducing words. |
is the free monoid product of |
You also need to eliminate ones. |
Some lemmas I found useful for leanprover-community#2578
This is now all in mathlib, in |
Define
free_monoid_product
as the quotient offree_monoid
by an appropriatecon
. This is a work in progress, and some proofs are not ready yet.