mathlib3

feat(computability): prove equivalence of NFAs and regular expressions

#14250

Open