Commit 2025-12-20 01:04 7478ffb2

View on Github →

chore: remove [NeZero n] assumptions in lemmas about Fin n (#33079) This PR removes [NeZero n] assumptions in lemmas about Fin n, in contexts where the lemmas have a parameter of type Fin n, whose existence implies that n can't be zero. This makes the statements a bit uglier with the haveIs but they're much easier to apply.

Estimated changes

Modified Mathlib/Data/Fin/Basic.lean

modified theorem Fin.cast_val_eq_self

added theorem Fin.neZero

modified theorem Fin.one_le_of_ne_zero

modified theorem Fin.val_add_one_of_lt'

modified theorem Fin.val_sub_one_of_ne_zero