Commit 2024-05-05 19:07 4d675c95

View on Github →

feat: Monotonicity of Nat.cast : Nat → Fin (n + 1) (#12652)

Estimated changes

deleted theorem Fin.cast_nat_eq_last
added theorem Fin.natCast_eq_last
added theorem Fin.natCast_le_natCast
added theorem Fin.natCast_lt_natCast
added theorem Fin.natCast_mono
added theorem Fin.natCast_strictMono