Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-03 12:44 f1b54734

View on Github →

feat(data/list/basic): fin_range (#1159)

  • feat(data/list/basic): fin_range fin_range is like list.range but returns a list (fin n) instead of a list nat
  • Update basic.lean

Estimated changes

added def list.fin_range
added theorem list.length_fin_range
added theorem list.mem_fin_range
added theorem list.nodup_fin_range