Commit 2024-11-11 12:43 7bcb2276

View on Github →

feat(Data/Fin/Parity): add lemmas about parity of Fin numbers (#8960)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Nat.lean

added theorem Nat.add_one_lt_of_even

added theorem Nat.one_lt_of_ne_zero_of_even

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.val_add_eq_of_add_lt

Created Mathlib/Data/Fin/Parity.lean

added theorem Fin.even_iff

added theorem Fin.even_iff_imp

added theorem Fin.even_iff_of_even

added theorem Fin.even_of_odd

added theorem Fin.even_of_val

added theorem Fin.odd_iff

added theorem Fin.odd_iff_imp

added theorem Fin.odd_iff_of_even

added theorem Fin.odd_of_odd

added theorem Fin.odd_of_val