Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fin.of_nat'_eq_coe

Modification history

2023-01-11 15:23

src/data/fin/basic.lean

refactor(data/fin/basic): fin refactor to use ne_zero (#18107)

Added fin.of_nat'_eq_coe View on Github →