Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-09 08:28 aa1fa0b2

View on Github →

feat(data/option/basic): option valued choice operator (#7101)

Estimated changes

Modified src/data/option/basic.lean

added theorem option.choice_eq

added theorem option.choice_eq_none

added theorem option.choice_is_some_iff_nonempty