Commit 2025-06-09 09:08 fe653fb9

View on Github →

feat(Data/Fin): Fin.castLE on the result of a cast from Nat (#25083)

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

added theorem NeZero.of_ge

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.castLE_natCast