Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.arrow_unit_equiv_unit

Modification history

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