Commit 2023-12-22 20:59 090f9f77

View on Github →

chore(Computability/RegularExpressions): golf (#9218) Golf a proof. Also add Language.mem_kstar_iff_exists_nonempty.

Estimated changes

Modified Mathlib/Computability/Language.lean

added theorem Language.mem_kstar_iff_exists_nonempty

Modified Mathlib/Computability/RegularExpressions.lean

modified theorem RegularExpression.rmatch_iff_matches'