isPreprimitive_fixingSubgroup_insert_iff

English

Jordan's criterion giving IsMultiplyPreprimitive for n+2 from IsPreprimitive and a substructure.

Русский

Критерий Джордана по множественному.primitivity: IsMultiplyPreprimitive для n+2.

LaTeX

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

Lean4

@[to_additive]
theorem isPreprimitive_fixingSubgroup_insert_iff {a : α} {t : Set (ofStabilizer G a)} :
    IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t)))
        ↥(ofFixingSubgroup G (insert a (Subtype.val '' t))) ↔
      IsPreprimitive (fixingSubgroup (stabilizer G a) t) (ofFixingSubgroup (stabilizer G a) t) :=
  isPreprimitive_congr (fixingSubgroupInsertEquiv a t).surjective ofFixingSubgroup_insert_map_bijective

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