Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-30 13:52 33a323cd

View on Github →

feat(data/fin): lemmas about ordering and cons (#13044) This marks a few extra facts simp, since the analogous facts are simp for nat.

Estimated changes

added theorem fin.not_lt_zero
modified theorem fin.zero_le
added theorem fin.cons_le_cons