Theorem Fin.natCast_le_natCast

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_le_natCast View on Github →