Mathlib v3 is deprecated. Go to Mathlib v4

Def W_type.nat_α_equiv_punit_sum_punit

Modification history

2022-03-14 18:58
src/data/W/constructions.lean
feat(data/W/constructions): add constructions of W types (#12292) …
Added W_type.nat_α_equiv_punit_sum_punitView on Github →