Commit 2024-05-15 17:20 830a482b

View on Github →

chore: Remove algebra imports to Data.Fin.Basic (#12862) Move the algebraic instance on Fin n from Data.Fin.Basic to a new file Algebra.Group.Fin. I credit Yakov for https://github.com/leanprover-community/mathlib/pull/5010. The one bit of algebra that is still imported in Data.Fin.Basic is NeZero. This is in prevision of its future upstreaming to Batteries or Std.

Estimated changes

added theorem Fin.coe_sub_one
added theorem Fin.le_sub_one_iff
added theorem Fin.lt_sub_one_iff
added theorem Fin.neg_last
added theorem Fin.neg_natCast_eq_one
added theorem Fin.sub_one_lt_iff
deleted theorem Fin.coe_sub_one
deleted theorem Fin.le_sub_one_iff
deleted theorem Fin.lt_sub_one_iff
added theorem Fin.natCast_def
deleted theorem Fin.neg_last
deleted theorem Fin.neg_natCast_eq_one
deleted theorem Fin.sub_one_lt_iff