of_pow — Mathlib

English

For any natural n, if x^n is irrational, then x is irrational.

Русский

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

LaTeX

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

Lean4

theorem of_pow : ∀ n : ℕ, Irrational (x ^ n) → Irrational x
  | 0 => fun h => by
    rw [pow_zero] at h
    exact (h ⟨1, cast_one⟩).elim
  | n + 1 => fun h => by
    rw [pow_succ] at h
    exact h.mul_cases.elim (of_pow n) id

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