Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-16 21:56 698eb1e3

View on Github →

feat(data/fin/basic): add lemmas about fin.cast (#10329)

Estimated changes

added theorem fin.add_nat_cast
added theorem fin.cast_add_cast
added theorem fin.cast_add_nat_left
added theorem fin.cast_add_nat_right
added theorem fin.cast_add_nat_zero
added theorem fin.cast_cast_add_left
added theorem fin.cast_nat_add_left
added theorem fin.cast_nat_add_right
added theorem fin.cast_nat_add_zero
added theorem fin.cast_succ_eq
added theorem fin.nat_add_cast
added theorem fin.succ_cast_eq