Commit 2024-02-14 06:30 3984e585

View on Github →

chore(Data/Fin): move Fin.equiv_iff_eq (#10522) The new proof is longer but I need this lemma before Fintype for a future refactor, see #9794

Estimated changes

added theorem Fin.equiv_iff_eq
deleted theorem Fin.equiv_iff_eq