Mathlib v3 is deprecated. Go to Mathlib v4

Theorem sum.exists

Modification history

2021-12-31 07:44

src/data/sum/basic.lean

docs(data/sum/basic): Expand module docstring and cleanup (#11158) …

Deleted sum.exists View on Github →

2017-12-13 04:31

feat(data/ordinal): well ordering theorem …

Added sum.exists View on Github →