Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-30 03:07 07e46bcf

View on Github →

feat(data/fin): iff on add or sub across last-0 break (#15916)

Estimated changes

added theorem fin.add_one_le_iff
added theorem fin.add_one_lt_iff
added theorem fin.last_le_iff
added theorem fin.le_sub_one_iff
added theorem fin.le_zero_iff
added theorem fin.lt_add_one_iff
added theorem fin.lt_sub_one_iff
added theorem fin.sub_one_lt_iff