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 Mathlib/Algebra/NeZero.lean

added theorem Nat.pos_of_neZero

Modified Mathlib/Control/Random.lean

Modified Mathlib/Data/Fin/Basic.lean

modified theorem Fin.last_pos'

modified def Fin.modNat

modified theorem Fin.one_lt_last

Modified Mathlib/Data/Fin/OrderHom.lean

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Nat/SuccPred.lean