Revision #2646 → #3768 · back to history
modifiedSequence (informal)ef33b5894c49
| Field | From #2646 | To #3768 |
|---|
| note | Mathlib's `Seq α` models a possibly-finite-or-infinite ordered sequence (with `Stream'`/`List` for the purely infinite/finite cases). | Mathlib's `Stream'.Seq α` models a possibly-finite-or-infinite ordered sequence (with `Stream'`/`List` for the purely infinite/finite cases). |
addedStrictly monotonically increasing1975a565ea78
modifiedExact sequence893cff247c77
| Field | From #2646 | To #3768 |
|---|
| mathlib.module | Mathlib.Algebra.Exact | Mathlib.Algebra.Exact.Basic |