Theorem Function.Embedding.embFinTwo_apply_one

Modification history

2025-05-18 18:58
Mathlib/Data/Fin/Tuple/Embedding.lean
feat(GroupTheory/GroupAction/MultiplePretransitivity): define multiply transitive actions (#23386) …
Added Function.Embedding.embFinTwo_apply_oneView on Github →