Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-22 14:51 8d71ec99

View on Github →

chore(data/fin): a few more lemmas about fin.insert_nth (#5079)

Estimated changes

added theorem fin.insert_nth_le_iff
added theorem fin.insert_nth_mem_Icc
added theorem fin.le_insert_nth_iff