English
If G acts pretransitively on α, then for any a,b ∈ α and any n, IsMultiplyPretransitive (stabilizer G a) (ofStabilizer G a) n holds if and only if IsMultiplyPretransitive (stabilizer G b) (ofStabilizer G b) n holds.
Русский
Если G действует предтранситивно на α, то для любых a,b ∈ α и любого n справедлива эквивалентность: IsMultiplyPretransitive (stabilizer G a) (ofStabilizer G a) n и IsMultiplyPretransitive (stabilizer G b) (ofStabilizer G b) n.
LaTeX
$$$IsMultiplyPretransitive\, (stabilizer\ G\ a)\ (ofStabilizer\ G\ a)\ n\iff IsMultiplyPretransitive\, (stabilizer\ G\ b)\ (ofStabilizer\ G\ b)\ n$$$
Lean4
@[to_additive]
theorem isMultiplyPretransitive_iff [IsPretransitive G α] {n : ℕ} {a b : α} :
IsMultiplyPretransitive (stabilizer G a) (ofStabilizer G a) n ↔
IsMultiplyPretransitive (stabilizer G b) (ofStabilizer G b) n :=
let ⟨_, hg⟩ := exists_smul_eq G a b
isMultiplyPretransitive_iff_of_conj hg.symm
