Theorem Fin.castLE_natCast

Modification history

2025-06-09 09:08
Mathlib/Data/Fin/Basic.lean
feat(Data/Fin): `Fin.castLE` on the result of a cast from `Nat` (#25083)
Added Fin.castLE_natCastView on Github →