inv_natCast_cpow_ofReal_pos — Mathlib

English

If n ≠ 0 and x ∈ ℝ, then ((n^x))⁻¹ is positive (as a complex number).

Русский

Если n ≠ 0 и x ∈ ℝ, то ((n^x))⁻¹ положительно (как комплексное число).

LaTeX

$$Let n ≠ 0 and x ∈ ℝ. 0 < ((n : ℂ) ^ (x : ℂ))^{-1}.$$

Lean4

theorem inv_natCast_cpow_ofReal_pos {n : ℕ} (hn : n ≠ 0) (x : ℝ) : 0 < ((n : ℂ) ^ (x : ℂ))⁻¹ :=
  by
  refine RCLike.inv_pos_of_pos ?_
  rw [show (n : ℂ) ^ (x : ℂ) = (n : ℝ) ^ (x : ℂ) from rfl, ← ofReal_cpow n.cast_nonneg']
  positivity

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