Commit 2025-04-03 12:47 7927ae7e

View on Github →

feat(Order): LTSeries can be extended to CovBy-RelSeries (#21803)

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.castSucc_castAdd

added theorem Fin.castSucc_natAdd

added theorem Fin.succ_castAdd

added theorem Fin.succ_natAdd

Modified Mathlib/Order/JordanHolder.lean

Modified Mathlib/Order/OrderIsoNat.lean

added theorem exists_covBy_seq_of_wellFoundedLT_wellFoundedGT_of_le

Modified Mathlib/Order/RelSeries.lean

added theorem LTSeries.exists_relSeries_covBy

modified theorem RelSeries.smash_castAdd

added theorem RelSeries.smash_castLE