Theorem Fin.even_add_one_iff_odd

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.even_add_one_iff_oddView on Github →
2024-12-10 02:18
Mathlib/Data/Fin/Parity.lean
feat(Data/Fin): Add lemmas `Fin.odd_add_one_iff_even` and `Fin.even_add_one_iff_odd` (#19815)
Added Fin.even_add_one_iff_oddView on Github →