Commit 2025-04-18 07:31 f8ca9db6

View on Github →

chore(Fin/Parity): move {n : ℕ} {k : Fin n} to variable (#24153)

Estimated changes

Modified Mathlib/Data/Fin/Parity.lean

modified theorem Fin.even_add_one_iff_odd

modified theorem Fin.even_iff

modified theorem Fin.even_iff_imp

modified theorem Fin.even_iff_mod_of_even

modified theorem Fin.even_iff_of_even

modified theorem Fin.even_of_odd

modified theorem Fin.even_of_val

modified theorem Fin.not_even_iff_odd_of_even

modified theorem Fin.not_odd_iff_even_of_even

modified theorem Fin.odd_add_one_iff_even

modified theorem Fin.odd_iff

modified theorem Fin.odd_iff_imp

modified theorem Fin.odd_iff_mod_of_even

modified theorem Fin.odd_iff_of_even

modified theorem Fin.odd_of_odd

modified theorem Fin.odd_of_val