of_zpow — Mathlib

English

For any integer m, if x^m is irrational, then x is irrational.

Русский

Для любого целого m, если x^m иррационально, то x иррационален.

LaTeX

$$$\forall m \in \mathbb{Z}, \; \operatorname{Irrational}(x^m) \Rightarrow \operatorname{Irrational}(x)$$$

Lean4

theorem of_zpow : ∀ m : ℤ, Irrational (x ^ m) → Irrational x
  | (n : ℕ) => fun h => by
    rw [zpow_natCast] at h
    exact h.of_pow _
  | -[n+1] => fun h => by
    rw [zpow_negSucc] at h
    exact h.of_inv.of_pow _

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