Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-06-05 08:10
c1e640b7
View on Github →
chore: fix names for String lemmas (
#13525
)
Estimated changes
Modified
Mathlib/Data/String/Basic.lean
modified
theorem
List.asString_eq
modified
theorem
List.asString_inj
modified
theorem
List.length_asString
added
theorem
List.toList_asString
deleted
theorem
List.toList_inv_asString
deleted
theorem
String.asString_inv_toList
added
theorem
String.asString_nil
added
theorem
String.asString_toList
deleted
theorem
String.nil_asString_eq_empty
Modified
Mathlib/Data/String/Defs.lean
deleted
def
String.getRest