Commit 2024-11-13 09:53 a98955ee

View on Github →

feat(Data/Fin): Add lemmas Fin.even_iff_mod_of_even and Fin.odd_iff_mod_of_even (#18941)

Estimated changes

Modified Mathlib/Data/Fin/Parity.lean

added theorem Fin.even_iff_mod_of_even

added theorem Fin.odd_iff_mod_of_even