Commit 2025-07-04 23:38 cdc3f005

View on Github →

chore(Fin): replace cast_add → castAdd, nat_add → natAdd in lemma names (#26764) This was mis-ported, the lemma names should match Fin.castAdd and Fin.natAdd.

Estimated changes

Modified Mathlib/Data/Fin/Tuple/Basic.lean

added theorem Fin.snoc_castAdd

deleted theorem Fin.snoc_cast_add

added theorem Fin.snoc_comp_castAdd

deleted theorem Fin.snoc_comp_cast_add

added theorem Fin.snoc_comp_natAdd

deleted theorem Fin.snoc_comp_nat_add