Commit 2022-03-01 10:48 f472efc9

View on Github →

chore: bump to nightly-2022-03-01 (#216)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

added theorem List.eq_of_mem_repeat'

deleted theorem List.eq_of_mem_repeat

added theorem List.get_append_right'

deleted theorem List.get_append_right

added theorem List.get_repeat'

deleted theorem List.get_repeat

modified theorem List.leftpad_prefix

added theorem List.mem_repeat'

deleted theorem List.mem_repeat

added theorem List.repeat'_succ

deleted theorem List.repeat_succ

Modified Mathlib/Data/Nat/Basic.lean

deleted theorem Nat.eq_of_mul_eq_mul_right

Modified Mathlib/Data/String/Defs.lean

added def String.repeat'

deleted def String.repeat

Modified Mathlib/Data/String/Lemmas.lean

modified theorem String.leftpad_prefix

added theorem String.length_repeat'

deleted theorem String.length_repeat

Modified Mathlib/Init/Data/List/Basic.lean

added def List.repeat'

deleted def List.repeat

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

added theorem List.length_repeat'

deleted theorem List.length_repeat

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

Modified Mathlib/Logic/Basic.lean

modified theorem heq_iff_eq

Modified Mathlib/Util/Simp.lean

Modified lean-toolchain