Commit 2024-07-27 16:57 286821d4

View on Github →

chore: qualify uses of ext and ext_iff lemmas (#15106) These will become protected in lean v4.11; it is easier to land these preparations in advance.

Estimated changes

modified theorem Fin.castAdd_inj
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 theorem Fin.pred_last
modified theorem Fin.succ_injective