Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-05 03:46 37f343cf

View on Github →

chore(data/stream): merge basic into init (#10617)

Estimated changes

Modified src/combinatorics/hindman.lean

Modified src/data/seq/seq.lean

Deleted src/data/stream/basic.lean

deleted theorem stream.head_drop

Modified src/data/stream/init.lean

added theorem stream.head_drop

Modified test/ext.lean