inv_pow — Mathlib

English

For any a ∈ α and n ∈ ℕ, (a^{-1})^{n} = (a^{n})^{-1}.

Русский

Для любого a ∈ α и n ∈ ℕ, (a^{-1})^{n} = (a^{n})^{-1}.

LaTeX

$$$(a^{-1})^{n} = (a^{n})^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_pow (a : α) : ∀ n : ℕ, a⁻¹ ^ n = (a ^ n)⁻¹
  | 0 => by rw [pow_zero, pow_zero, inv_one]
  | n + 1 => by
    rw [pow_succ', pow_succ, inv_pow _ n, mul_inv_rev]
      -- the attributes are intentionally out of order. `smul_zero` proves `zsmul_zero`.

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