[Merged by Bors] - feat(data/list/basic): repeat injectivity #6337
Conversation
pechersky
commented
Feb 21, 2021
pechersky
commented
pechersky
added
the
awaiting-review
src/data/list/basic.lean
Outdated
| @@ -474,6 +474,35 @@ by cases n; refl | |||
| @[simp] theorem join_repeat_nil (n : ℕ) : join (repeat [] n) = @nil α := | |||
| by induction n; [refl, simp only [*, repeat, join, append_nil]] | |||
|
|
|||
| lemma repeat_inj_left {a b : α} {n : ℕ} (npos : 0 < n) | |||
There was a problem hiding this comment.
It looks like *_left_inj and *_right_inj are more common in the library, and the example at our naming conventions page is sub_right_inj, so I'd recommend switching the naming over to that.
This convention might be confusing given all the other things named with left and right at the very end, but that's something we should discuss on Zulip if someone feels strongly about it.
There was a problem hiding this comment.
I renamed lemmas, added function.injective versions, and golfed the proofs.
|
Thanks! Feel free to merge if you're happy with Yury's changes. |
|
✌️ pechersky can now approve this pull request. To approve and merge a pull request, simply reply with |
bryangingechen
added
delegated
|
bors r+ |
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
