Theorems · Theorem · group theory
Set.powersetCard.mulActionHom_of_embedding_surjective
∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] {n : ℕ} [inst_2 : DecidableEq α],
Function.Surjective ⇑(Set.powersetCard.mulActionHom_of_embedding G α n)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupMulActionDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Finsetstatement and proof · cited by 13,712
- Set.Elemstatement and proof · cited by 7,166
- Groupstatement and proof · cited by 6,238
- Finset.univproof · cited by 3,473
- Fintype.cardproof · cited by 1,386
- MulActionstatement and proof · cited by 1,294
- Function.Embeddingstatement and proof · cited by 988
- Finset.mapproof · cited by 747
- Fintype.card_finproof · cited by 270
- MulActionHomstatement · cited by 124
- Set.powersetCardstatement and proof · cited by 100
Cited by1
Results whose statement or proof uses this declaration.
- Set.powersetCard.isPretransitive_of_isMultiplyPretransitiveproof · cited by 2