Commit 2024-12-10 02:18 87828655

View on Github →

feat(Data/Fin): Add lemmas Fin.odd_add_one_iff_even and Fin.even_add_one_iff_odd (#19815)

Estimated changes

Modified Mathlib/Data/Fin/Parity.lean

added theorem Fin.even_add_one_iff_odd

added theorem Fin.odd_add_one_iff_even