pow_disjoint_pow — Mathlib

English

If σ and τ are disjoint, then for natural exponents m, n, the powers σ^m and τ^n are disjoint.

Русский

Если σ и τ разнесены, то для натуральных степеней m, n перестановки σ^m и τ^n разнесены.

LaTeX

$$$$ \forall \sigma, \tau\ (\operatorname{Disjoint}(\sigma,\tau)\Rightarrow \forall m,n\in \mathbb{N},\ \operatorname{Disjoint}(\sigma^m,\tau^n)). $$$$

Lean4

theorem pow_disjoint_pow {σ τ : Perm α} (hστ : Disjoint σ τ) (m n : ℕ) : Disjoint (σ ^ m) (τ ^ n) :=
  hστ.zpow_disjoint_zpow m n

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