isMultiplyPretransitive_iff — Mathlib

English

If IsPretransitive holds for the fixingSubgroup and its image, then the corresponding subgroup is IsMultiplyPreprimitive.

Русский

Если выполняется предтранситивность для фиксационной подгруппы и её образа, то соответствующая подгруппа является IsMultiplyPreprimitive.

LaTeX

$$IsMultiplyPreprimitive (fixingSubgroup G s) (SubMulAction.ofFixingSubgroup G s) n$$

Lean4

@[to_additive]
theorem isMultiplyPretransitive_iff {n : ℕ} : IsMultiplyPretransitive G α n ↔ ∀ x y : Fin n ↪ α, ∃ g : G, g • x = y :=
  isPretransitive_iff _ _

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