Commit 2024-05-23 11:18 dff169d7

View on Github →

chore: Remove order dependencies to Data.Fin.Basic (#13005) Move all the declarations using the mathlib order hierarchy to a new file Order.Fin. There were a bunch of order embeddings in Data.Fin.Basic, so I kept an embedding version of them around and renamed the order embedding version.

Estimated changes

added def unitsEquivNeZero
modified def Fin.addNatEmb
deleted theorem Fin.antitone_iff_succ_le
deleted theorem Fin.bot_eq_zero
modified def Fin.castAddEmb
added theorem Fin.castAdd_inj
added theorem Fin.castAdd_injective
deleted def Fin.castIso
deleted theorem Fin.castIso_refl
deleted theorem Fin.castIso_to_equiv
modified def Fin.castLEEmb
modified theorem Fin.castLE_inj
modified theorem Fin.castLE_injective
modified theorem Fin.castLT_eq_castPred
modified theorem Fin.castPred_castSucc
modified theorem Fin.castPred_one
modified theorem Fin.castPred_zero'
modified theorem Fin.castPred_zero
modified def Fin.castSuccEmb
modified theorem Fin.castSucc_injective
modified theorem Fin.castSucc_lt_or_lt_succ
added theorem Fin.coe_castLEEmb
added theorem Fin.coe_castSuccEmb
deleted theorem Fin.coe_orderIso_apply
deleted theorem Fin.monotone_iff_le_succ
deleted theorem Fin.monotone_pred_comp
modified def Fin.natAddEmb
deleted theorem Fin.orderEmbedding_eq
deleted def Fin.orderIsoSubtype
modified theorem Fin.pred_last
deleted def Fin.revOrderIso
deleted theorem Fin.strictMono_addNat
deleted theorem Fin.strictMono_castAdd
deleted theorem Fin.strictMono_castLE
deleted theorem Fin.strictMono_castSucc
deleted theorem Fin.strictMono_natAdd
deleted theorem Fin.strictMono_pred_comp
deleted theorem Fin.strictMono_succ
deleted theorem Fin.strictMono_unique
modified def Fin.succEmb
modified theorem Fin.succ_injective
deleted theorem Fin.symm_castIso
deleted theorem Fin.top_eq_last
deleted theorem Fin.val_strictMono
added def finCongr
added theorem finCongr_apply_coe
added theorem finCongr_apply_mk
added theorem finCongr_eq_equivCast
added theorem finCongr_refl
added theorem finCongr_symm
modified theorem Fin.repeat_one
modified theorem Matrix.empty_vecAppend
modified def Matrix.vecAlt0
modified theorem Finsupp.cons_support
deleted def unitsEquivNeZero
modified theorem Fin.Iio_castSucc
modified theorem Fin.Iio_last_eq_map
modified theorem Fin.Ioi_succ
modified theorem Fin.Ioi_zero_eq_map
modified theorem Cycle.subsingleton_nil
modified def TensorPower.cast
deleted def finCongr
deleted theorem finCongr_apply_coe
deleted theorem finCongr_apply_mk
deleted theorem finCongr_symm
deleted theorem finCongr_symm_apply_coe
modified theorem finRotate_last'
modified theorem finRotate_succ
added theorem Fin.bot_eq_zero
added def Fin.castOrderIso
added theorem Fin.castOrderIso_refl
added theorem Fin.coe_orderIso_apply
added theorem Fin.coe_succOrderEmb
added theorem Fin.monotone_pred_comp
added theorem Fin.orderEmbedding_eq
added def Fin.revOrderIso
added theorem Fin.strictMono_addNat
added theorem Fin.strictMono_castAdd
added theorem Fin.strictMono_castLE
added theorem Fin.strictMono_natAdd
added theorem Fin.strictMono_succ
added theorem Fin.strictMono_unique
added def Fin.succOrderEmb
added theorem Fin.symm_castOrderIso
added theorem Fin.top_eq_last
added def Fin.valOrderEmb
added theorem Fin.val_strictMono