Theorem Fin.odd_of_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.odd_of_oddView on Github →
2024-11-11 12:43
Mathlib/Data/Fin/Parity.lean
feat(Data/Fin/Parity): add lemmas about parity of `Fin` numbers (#8960)
Added Fin.odd_of_oddView on Github →