isPreprimitive_ofFixingSubgroup_conj_iff

English

If hG IsPreprimitive and s has |s|=n+1 with a preprimitive fixing-subgroup, then IsMultiplyPreprimitive for n+2.

Русский

Если hG IsPreprimitive и |s|=n+1, а fixingSubgroup предварительно примитивна, то IsMultiplyPreprimitive для n+2.

LaTeX

$$IsMultiplyPreprimitive G α (n+2)$$

Lean4

@[to_additive]
theorem isPreprimitive_ofFixingSubgroup_conj_iff {s : Set α} {g : G} :
    IsPreprimitive (fixingSubgroup G s) (ofFixingSubgroup G s) ↔
      IsPreprimitive (fixingSubgroup G (g • s)) (ofFixingSubgroup G (g • s)) :=
  isPreprimitive_congr (fixingSubgroupEquivFixingSubgroup rfl).surjective conjMap_ofFixingSubgroup_bijective

Похожие утверждения