Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.nat_equiv_nat_sum_unit

Modification history

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