Commit 2025-01-20 15:19 3f57df84

feat: Myhill–Nerode theorem (#11311) I take a different approach to the lean-automata version by @atarnoam. Rather than taking a Quotient by the Nerode relation, I instead talk about the the function leftQuotient := fun x => { y | x ++ y ∈ L }. This is more direct as it avoids going through the Quotient API. The Nerode relation can be defined later (not in this PR) as the kernel of this function.