inv_pow — Mathlib

English

For every a ∈ ENNReal and every n ∈ ℕ, (a^n)⁻¹ = (a⁻¹)^n.

Русский

Для всех a ∈ ENNReal и n ∈ ℕ выполняется (a^n)⁻¹ = (a⁻¹)^n.

LaTeX

$$\forall a \in \mathbb{R}_{\ge 0}^{\infty}, \forall n \in \mathbb{N}, (a^n)^{-1} = (a^{-1})^n$$

Lean4

protected theorem inv_pow : ∀ {a : ℝ≥0∞} {n : ℕ}, (a ^ n)⁻¹ = a⁻¹ ^ n
  | _, 0 => by simp only [pow_zero, inv_one]
  | ⊤, n + 1 => by simp [top_pow]
  | (a : ℝ≥0), n + 1 => by
    rcases eq_or_ne a 0 with (rfl | ha)
    · simp [top_pow]
    · have := pow_ne_zero (n + 1) ha
      norm_cast
      rw [inv_pow]

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