zpow_mem — Mathlib

English

If x ∈ K for a subgroup K, then x^n ∈ K for every integer n.

Русский

Если x ∈ K, то x^n ∈ K для каждого целого числа n.

LaTeX

$$x \in K \Rightarrow x^{n} \in K \quad \forall n \in \mathbb{Z}$$

Lean4

@[to_additive (attr := aesop 90% (rule_sets := [SetLike]))]
theorem zpow_mem {x : M} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K
  | (n : ℕ) => by
    rw [zpow_natCast]
    exact pow_mem hx n
  | -[n+1] => by
    rw [zpow_negSucc]
    exact inv_mem (pow_mem hx n.succ)

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