zpow_right — Mathlib

English

If a semiconjugates x to y in a group, then for every integer m, a semiconjugates x^{m} to y^{m}. In particular, a x^{m} = y^{m} a for all m ∈ Z.

Русский

Если a полуSопряжает x к y в группе, тогда для любого целого m верно, что a сопряжает x^{m} к y^{m}. То есть для всех m ∈ Z выполняется a x^{m} = y^{m} a.

LaTeX

$$$$\forall m\in \mathbb{Z}:\ SemiconjBy\ a\ x^{m}\ y^{m}.$$$$

Lean4

@[to_additive (attr := simp)]
theorem zpow_right (h : SemiconjBy a x y) : ∀ m : ℤ, SemiconjBy a (x ^ m) (y ^ m)
  | (n : ℕ) => by simp [zpow_natCast, h.pow_right n]
  | .negSucc n => by
    simp only [zpow_negSucc, inv_right_iff]
    apply pow_right h

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