Theorem Fin.Embedding.restrictSurjective_of_le_ENatCard

Modification history

2025-10-04 20:24
Mathlib/SetTheory/Cardinal/Embedding.lean
feat: a theorem of Jordan on primitive subgroups of the permutation group (#26282) …
Added Fin.Embedding.restrictSurjective_of_le_ENatCardView on Github →