Commit 2023-12-31 21:44 7d31d033

View on Github →

feat: Fin CharP and lemmas for Fin rollover (#9033)

Estimated changes

Modified Mathlib/Algebra/CharP/Basic.lean

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.add_one_le_of_lt

added theorem Fin.exists_eq_add_of_le

added theorem Fin.exists_eq_add_of_lt

added theorem Fin.neg_last

added theorem Fin.neg_nat_cast_eq_one

added theorem Fin.pos_of_ne_zero