Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-25 17:22 43e84cdd

View on Github →

feat(data/fin/succ_pred): fin is an archimedean succ/pred order (#12792)

Estimated changes

Modified src/algebra/big_operators/fin.lean

Modified src/data/fin/basic.lean

added theorem fin.coe_fin_one

added theorem fin.coe_neg_one

added theorem fin.coe_sub_one

added def order_iso.fin_equiv

added theorem order_iso.fin_equiv_apply

added theorem order_iso.fin_equiv_symm_apply

Created src/data/fin/succ_pred.lean

added theorem fin.pred_apply

added theorem fin.pred_eq

added theorem fin.succ_apply

added theorem fin.succ_eq

Modified src/data/fintype/basic.lean

deleted theorem fintype.linear_order.is_well_order

added theorem fintype.linear_order.is_well_order_gt

added theorem fintype.linear_order.is_well_order_lt

deleted theorem fintype.preorder.well_founded

added theorem fintype.preorder.well_founded_gt

added theorem fintype.preorder.well_founded_lt

Modified src/order/rel_classes.lean

Modified src/order/succ_pred/basic.lean

added def pred_order.of_core

added def succ_order.of_core

Modified src/set_theory/ordinal/basic.lean