Theorems · Theorem · group theory
Equiv.Perm.subgroup_eq_top_of_nontrivial
∀ {α : Type u_1} {G : Subgroup (Equiv.Perm α)} [Finite α], Nat.card α ≤ 2 → Nontrivial ↥G → G = ⊤- Defined in
- Mathlib.GroupTheory.GroupAction.Jordan
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Finite
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topstatement · cited by 9,680
- Subgroupstatement and proof · cited by 3,593
- LE.le.transproof · cited by 3,151
- Finitestatement and proof · cited by 3,029
- Nontrivialstatement and proof · cited by 2,416
- Equiv.Permstatement and proof · cited by 1,375
- Nat.cardstatement and proof · cited by 844
- Nat.card_permproof · cited by 10
- Nat.factorial_leproof · cited by 10
- Subgroup.nontrivial_iff_ne_botproof · cited by 7
- Nat.factorial_twoproof · cited by 6
- Subgroup.one_lt_card_iff_ne_botproof · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.