Theorem Fin.cast_strictMono

Modification history

2025-01-05 03:32

Mathlib/Order/Fin/Basic.lean

chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464)

Modified Fin.cast_strictMono View on Github →

2024-09-16 08:22

Mathlib/Order/Fin/Basic.lean

feat: missing basic API lemmas (#16842)

Added Fin.cast_strictMono View on Github →