Def equiv.nat_sum_unit_equiv_nat
Modification history
2018-09-15 17:29
data/equiv/basic.lean
feat(linear_algebra): dimension theorem (#345) …
Deleted equiv.nat_sum_unit_equiv_natView on Github →2018-03-29 17:23
data/equiv.lean
fix(.): unit is now an abbreviation: unit := punit.{1}
Modified equiv.nat_sum_unit_equiv_natView on Github →