Theorem Fin.natCast_eq_last

Modification history

2024-05-05 19:07
Mathlib/Data/Fin/Basic.lean
feat: Monotonicity of `Nat.cast : Nat → Fin (n + 1)` (#12652)
Added Fin.natCast_eq_lastView on Github →