Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-06 14:53 22f02c16

View on Github →

feat(data/{seq,stream}): enum and some helper API (#15790)

Estimated changes

added def seq.enum
added theorem seq.enum_cons
added theorem seq.enum_nil
added theorem seq.nth_enum
added theorem seq.nth_zip
added theorem seq.nth_zip_with
added theorem seq.val_cons
added def stream.enum
added theorem stream.enum_eq_zip
added theorem stream.nth_enum