Theorem Function.Embedding.exists_of_card_eq_finset

Modification history

2025-12-01 10:02
Mathlib/Data/Fintype/EquivFin.lean
feat(GroupTheory/GroupAction/SubMulAction/Combination): combinations and group actions (#27107) …
Added Function.Embedding.exists_of_card_eq_finsetView on Github →