Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-13 00:49 30c2c5bf

View on Github →

feat(data/fin): cast_succ_mk and other lemmas (#6094)

  • add lemmas for all the fin.cast_* functions which describe what happens to an "explicitly presented" term of fin n, built from the constructor
  • fixes some errors in doc-strings

Estimated changes

added theorem fin.cast_add_mk
added theorem fin.cast_le_mk
added theorem fin.cast_lt_mk
added theorem fin.cast_mk
added theorem fin.cast_succ_mk
added theorem fin.succ_mk