mathlib3
3c006126
- feat(data/{seq,stream}): cons_injective2 (#15832)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(data/{seq,stream}): cons_injective2 (#15832) Also some simple API lemmas for `nth` I didn't change the style of the `stream/init` file. Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
Author
vihdzp
Parents
87714908
Loading