Theorem Fin.addCases_castAdd_natAdd

Modification history

2026-06-17 15:42
Mathlib/Data/Fin/Tuple/Basic.lean
feat(Convert): less aggressive congruence (#38071) …
Modified Fin.addCases_castAdd_natAddView on Github →
2025-08-12 12:14
Mathlib/Data/Fin/Tuple/Basic.lean
feat(Data/Fin/Tuple): lemmas on appending finite sequences (#27577) …
Added Fin.addCases_castAdd_natAddView on Github →