Commit 2025-06-06 04:20 fc52fd8b

View on Github →

chore: remove global NatCast (Fin n) and CommRing (Fin n) instances. (#25476) This PR ensures there are no global NatCast (Fin n) instances

Estimated changes

added theorem Fin.intCast_def'
modified theorem Fin.coe_eq_castSucc
modified theorem Fin.coe_succ_lt_iff_lt
deleted theorem Fin.natCast_def
modified theorem Fin.ofNat_eq_cast
added def Fin.instCommRing