isMultiplyPretransitive_iff_of_conj

English

IsMultiplyPretransitive is preserved under conjugation along a translate b=g•a.

Русский

Пре-транситивность сохраняется при конъьюгации вдоль переноса b=g•a.

LaTeX

$$$IsMultiplyPretransitive\; (stabilizer\ G\ a)\ (ofStabilizer\ G\ a)\ n \iff\ IsMultiplyPretransitive\; (stabilizer\ G\ b)\ (ofStabilizer\ G\ b)\ n$, где $b=g\cdot a$$$

Lean4

@[to_additive]
theorem isMultiplyPretransitive_iff_of_conj {n : ℕ} {a b : α} {g : G} (hg : b = g • a) :
    IsMultiplyPretransitive (stabilizer G a) (ofStabilizer G a) n ↔
      IsMultiplyPretransitive (stabilizer G b) (ofStabilizer G b) n :=
  IsPretransitive.of_embedding_congr (MulEquiv.surjective _) (ofStabilizer.conjMap_bijective hg)

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