Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-12 01:34 3c006126

View on Github →

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.

Estimated changes

Modified src/data/seq/seq.lean

added theorem seq.cons_injective2

added theorem seq.cons_left_injective

added theorem seq.cons_right_injective

Modified src/data/stream/init.lean

added theorem stream.cons_injective2

added theorem stream.cons_injective_left

added theorem stream.cons_injective_right

added theorem stream.nth_succ_cons

modified theorem stream.nth_zero_cons