Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.bool_equiv_unit_sum_unit

Modification history

2018-09-15 17:29
data/equiv/basic.lean
feat(linear_algebra): dimension theorem (#345) …
Deleted equiv.bool_equiv_unit_sum_unitView on Github →
2018-03-29 17:23
data/equiv.lean
fix(.): unit is now an abbreviation: unit := punit.{1}
Modified equiv.bool_equiv_unit_sum_unitView on Github →
2017-09-08 14:49
data/equiv.lean
feat(data/equiv): port data/equiv.lean from Lean2
Added equiv.bool_equiv_unit_sum_unitView on Github →