Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-16 19:39 4f42fbf1

View on Github →

feat(data/option): more option stuff

Estimated changes

Modified algebra/big_operators.lean

Modified algebra/group.lean

modified def is_group_hom

Modified data/list/basic.lean

added theorem option.to_list_nodup

Modified data/option.lean

modified theorem option.bind_eq_some

modified theorem option.bind_some

added theorem option.get_mem

added theorem option.get_of_mem

modified theorem option.guard_eq_some

added theorem option.iget_mem

added theorem option.iget_of_mem

added theorem option.iget_some

modified theorem option.is_none_iff_eq_none

modified theorem option.is_some_iff_exists

modified theorem option.map_eq_some

modified theorem option.map_id'

modified theorem option.map_none

modified theorem option.map_some

modified theorem option.mem_def

added theorem option.mem_to_list

modified theorem option.none_bind

modified theorem option.seq_some

modified theorem option.some_bind

modified theorem option.some_inj