Commit 2021-10-11 17:57 fded0944

View on Github →

feat(List/String leftpad) (#66)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Basic.lean

added def List.isInfix

added def List.isPrefix

added def List.isSuffix

added def List.leftpad

added theorem List.leftpad_length

added theorem List.leftpad_prefix

added theorem List.leftpad_suffix

added theorem List.length_repeat

Created Mathlib/Data/String/Defs.lean

added def String.isPrefix

added def String.isSuffix

added def String.leftpad

added def String.repeat

Created Mathlib/Data/String/Lemmas.lean

added theorem String.congr_append

added theorem String.leftpad_length

added theorem String.leftpad_prefix

added theorem String.leftpad_suffix

added theorem String.length_append

added theorem String.length_eq_list_length

added theorem String.length_repeat

Modified Mathlib/Init/Data/Nat/Lemmas.lean