English
If a G-action on X is pretransitive and X has prime cardinality, then the action is preprimitive.
Русский
Если действие G на X претривитивно и кардинал X — простое число, тогда действие является предпримитивным.
LaTeX
$$IsPretransitive(G,X) ∧ Prime(card(X)) ⇒ IsPreprimitive(G,X)$$
Lean4
/-- A pretransitive action on a set of prime order is preprimitive -/
@[to_additive /-- A pretransitive action on a set of prime order is preprimitive -/
]
theorem of_prime_card [hGX : IsPretransitive G X] (hp : Nat.Prime (Nat.card X)) : IsPreprimitive G X :=
by
refine ⟨fun {B} hB ↦ B.subsingleton_or_nontrivial.imp id fun hB' ↦ ?_⟩
have : Finite X := (Nat.card_ne_zero.mp hp.ne_zero).2
rw [Set.eq_univ_iff_ncard, eq_comm, ← hp.dvd_iff_eq ((Set.one_lt_ncard).mpr hB').ne']
exact hB.ncard_dvd_card hB'.nonempty
