Commit 2024-05-13 07:14 2c9afeb5

View on Github →

chore: Reduce imports to Data.Fin.Basic (#12828) By using Nat and Int specific lemmas, we can reduce the import to Data.Fin.Basic to almost nothing. I haven't gone all the way to removing all dependencies because that involves moving declarations around and I would like to keep the diff clean.

Estimated changes

modified theorem Fin.last_pos'
modified def Fin.modNat
modified theorem Fin.one_lt_last