Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.option_equiv_sum_unit

Modification history

2018-09-15 17:29
data/equiv/basic.lean
feat(linear_algebra): dimension theorem (#345) …
Deleted equiv.option_equiv_sum_unitView on Github →
2018-03-29 17:23
data/equiv.lean
fix(.): unit is now an abbreviation: unit := punit.{1}
Modified equiv.option_equiv_sum_unitView on Github →
2017-09-19 02:55
data/equiv.lean
refactor(data/equiv,encodable): refactor/simplify proofs
Added equiv.option_equiv_sum_unitView on Github →