Theorem Fin.odd_iff_mod_of_even

Modification history

2025-04-18 07:31
Mathlib/Data/Fin/Parity.lean
chore(Fin/Parity): move `{n : ℕ} {k : Fin n}` to `variable` (#24153)
Modified Fin.odd_iff_mod_of_evenView on Github →
2024-11-13 09:53
Mathlib/Data/Fin/Parity.lean
feat(Data/Fin): Add lemmas `Fin.even_iff_mod_of_even` and `Fin.odd_iff_mod_of_even` (#18941)
Added Fin.odd_iff_mod_of_evenView on Github →