English
If n.succ ≤ ENat.card α and IsMultiplyPretransitive M α n.succ, then IsMultiplyPreprimitive M α n.
Русский
Если n.succ ≤ ENat.card α и IsMultiplyPretransitive M α n.succ, то IsMultiplyPreprimitive M α n.
LaTeX
$$IsMultiplyPreprimitive M α n$$
Lean4
/-- `n.succ`-pretransitivity implies `n`-preprimitivity. -/
@[to_additive /-- `n.succ`-pretransitivity implies `n`-preprimitivity. -/
]
theorem isMultiplyPreprimitive_of_isMultiplyPretransitive_succ {n : ℕ} (hα : ↑n.succ ≤ ENat.card α)
[IsMultiplyPretransitive M α n.succ] : IsMultiplyPreprimitive M α n :=
by
rcases Nat.eq_zero_or_pos n with hn | hn
· rw [hn]
exact is_zero_preprimitive M α
rw [isMultiplyPreprimitive_iff]
constructor
· exact isMultiplyPretransitive_of_le' (Nat.le_succ n) hα
· intro s hs
obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le hn
apply isPreprimitive_of_is_two_pretransitive
have hs' : s.encard = m := by
simp [hm, add_comm 1] at hs
exact ENat.add_left_injective_of_ne_top ENat.one_ne_top hs
have : Finite s := Set.finite_of_encard_eq_coe hs'
apply ofFixingSubgroup.isMultiplyPretransitive (G := M) s (n := n.succ)
simp [Set.ncard, hs', hm, add_comm 1]
