Theorem Fin.veq_of_eq

Modification history

2024-08-14 01:35
Mathlib/Init/Data/Fin/Basic.lean
chore: delete `Init.Data.Fin.Basic` (#15762)
Deleted Fin.veq_of_eqView on Github →
2024-06-10 06:26
Mathlib/Init/Data/Fin/Basic.lean
chore(*): fix more deprecated dates (#13674)
Modified Fin.veq_of_eqView on Github →
2024-03-01 13:29
Mathlib/Init/Data/Fin/Basic.lean
chore(Init/Fin): deprecate `Fin.eq_of_veq` and `Fin.veq_of_eq` (#10626) …
Modified Fin.veq_of_eqView on Github →
2022-11-03 02:45
Mathlib/Init/Data/Fin/Basic.lean
feat: port Logic.Unique (#512)
Added Fin.veq_of_eqView on Github →