Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-22 00:01 b8b87559

View on Github →

feat(data/list/basic): repeat injectivity (#6337)

Estimated changes

modified theorem list.eq_of_mem_repeat
added theorem list.mem_repeat
added theorem list.repeat_left_inj'
added theorem list.repeat_left_inj
added theorem list.repeat_right_inj