Theorem Fin.not_even_iff_odd_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.not_even_iff_odd_of_evenView on Github →
2024-11-14 01:18
Mathlib/Data/Fin/Parity.lean
feat(Data/Fin): Add lemmas `Fin.not_odd_iff_even_of_even` and `Fin.not_even_iff_odd_of_even` (#18960)
Added Fin.not_even_iff_odd_of_evenView on Github →