zpow_right₀ — Mathlib

English

For a group with zero, SemiconjBy a x y remains under integer powers: for all m ∈ Z, SemiconjBy a (x^m) (y^m).

Русский

Для группы с нулём SemiconjBy a x y сохраняется при целочисленных степенях: для всех m ∈ Z, SemiconjBy a (x^m) (y^m).

LaTeX

$$$\forall m \in \mathbb{Z},\; SemiconjBy\ a\ (x^{m})\ (y^{m})$$$

Lean4

theorem zpow_right₀ {a x y : G₀} (h : SemiconjBy a x y) : ∀ m : ℤ, SemiconjBy a (x ^ m) (y ^ m)
  | (n : ℕ) => by simp [h.pow_right n]
  | .negSucc n => by simp only [zpow_negSucc, (h.pow_right (n + 1)).inv_right₀]

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