Theorems · Theorem · number theory

Fin.odd_iff

∀ {n : ℕ} {k : Fin n} [inst : NeZero n], Odd k ↔ Odd n ∨ Odd ↑k

In Fin n, all elements are odd for odd n, otherwise an element is odd iff its Fin.val value is odd.

Defined in

Mathlib.Data.Fin.Parity

Cited by

1 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NeZero