Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-07 20:04 b173925a

View on Github →

refactor(data/fin): use order_embedding for many maps (#5251) Also swap data.fin with order.rel_iso in the import tree.

Estimated changes

modified def fin.add_nat
modified def fin.cast
modified def fin.cast_add
modified def fin.cast_le
deleted theorem fin.cast_le_injective
modified theorem fin.cast_lt_cast_succ
modified def fin.cast_succ
modified theorem fin.cast_succ_inj
modified theorem fin.coe_add_nat
modified theorem fin.coe_cast
modified theorem fin.coe_cast_add
modified theorem fin.coe_cast_le
modified theorem fin.coe_cast_lt
modified theorem fin.coe_cast_succ
modified theorem fin.coe_last
added theorem fin.coe_nat_add
deleted theorem fin.coe_sub_nat
added theorem fin.coe_succ_embedding
modified def fin.nat_add
modified def fin.sub_nat
modified def fin.succ_above
added theorem fin.succ_above_aux
modified theorem fin.succ_above_zero
added theorem fin.symm_cast