Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fin.default_fin_one

Modification history

2020-11-22 22:06
src/data/fin.lean
chore(logic/unique): add `fin.inhabited` (#5077)
Deleted fin.default_fin_oneView on Github →
2020-11-20 12:39
src/data/fin.lean
feat(measure_theory/lp_space): prove that neg and add are in Lp (#5014) …
Added fin.default_fin_oneView on Github →