Theorem Fin.cast_eq_self

Modification history

2025-01-05 03:32

Mathlib/Data/Fin/Basic.lean

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

Modified Fin.cast_eq_self View on Github →

2023-12-27 19:55

Mathlib/Data/Fin/Basic.lean

feat: add lemmas about `Fin.rev` (#8814)

Added Fin.cast_eq_self View on Github →