Theorem Fin.Embedding.snoc_castSucc

Modification history

2025-05-18 18:58
Mathlib/Data/Fin/Tuple/Embedding.lean
feat(GroupTheory/GroupAction/MultiplePretransitivity): define multiply transitive actions (#23386) …
Modified Fin.Embedding.snoc_castSuccView on Github →
2025-05-16 03:37
Mathlib/Data/Fin/Tuple/Embedding.lean
feat(Data/Fin/Tuple/Embedding): create embeddings of Fin Nat to types (#24167) …
Added Fin.Embedding.snoc_castSuccView on Github →