Commit 2025-08-12 12:14 0e0e525e

View on Github →

feat(Data/Fin/Tuple): lemmas on appending finite sequences (#27577) Prove simple results regarding appending and de-appending of finite sequences. Used to define conical combinations and the conical hull (subsequent PR).

Estimated changes

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

added theorem Fin.addCases_castAdd_natAdd

added theorem Fin.forall_fin_add

added theorem Fin.forall_fin_add_pi