Commit 2024-08-14 01:35 4525315b

View on Github →

chore: delete Init.Data.Fin.Basic (#15762)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/Range.lean

Deleted Mathlib/Init/Data/Fin/Basic.lean

deleted theorem Fin.eq_of_veq

deleted theorem Fin.ne_of_vne

deleted theorem Fin.veq_of_eq

deleted theorem Fin.vne_of_ne