Adding DFA regular expression equivalence to mathlib

Stream: new members

[Russell Emerine]

Hello y'all, I'm Russell, an undergrad at CMU. I have a working proof of the equivalence of regular expressions to DFAs. I'd like to add my proof to the lean 3 mathlib. How should I start a PR? I'd also like some opinions on how to formulate the key theorems and organize parts of the proofs, more details if anyone asks. Thanks to everyone here for running such an awesome project!

[Yaël Dillies]

Hey! @Fox Thomson and I had work towards it, so please show us so we can compare.

[Yaël Dillies]

Once the @maintainers have given you write access, you will be able to open a PR from the mathlib repo (not a fork).

[Eric Wieser]

(we can't give write access without a github username!)

[Bryan Gin-ge Chen]

Welcome! In case you haven't already seen it, we've got a page with some tips for new contributors: https://leanprover-community.github.io/contribute/index.html

[Russell Emerine]

Sorry, my github is just RussellEmerine

[Bryan Gin-ge Chen]

Russell Emerine said:

Sorry, my github is just RussellEmerine

Invite sent! https://github.com/leanprover-community/mathlib/invitations

[Russell Emerine]

i promise i'm working on this lol, there'll be new stuff in a new branch soon

[Russell Emerine]

Ok, now what I had already is on the branch RussellEmerine/DFA_equivalent_regular_expression. I'll be making some of the more obvious changes soon, please let me know if there's anything in particular that needs to be fixed or reorganized.