irrational_natCast_add_iff — Mathlib

English

Let n be a natural number and x a real number. The irrationality of n + x is equivalent to the irrationality of x.

Русский

Пусть n ∈ ℕ и x ∈ ℝ. Иррациональность числа n + x равносильна иррациональности x.

LaTeX

$$$\\forall n \\in \\mathbb{N}, x \\in \\mathbb{R}, \\operatorname{Irrational}(n + x) \\iff \\operatorname{Irrational}(x)$$$

Lean4

@[simp]
theorem irrational_natCast_add_iff : Irrational (n + x) ↔ Irrational x :=
  ⟨of_natCast_add n, fun h => h.natCast_add n⟩

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