irrational_sqrt_intCast_iff_of_nonneg

English

For integer z with z ≥ 0, sqrt(z) is irrational iff z is not a perfect square in integers.

Русский

Для целого z ≥ 0 корень z иррационален тогда и тогда, когда z не является квадратом целого числа.

LaTeX

$$$\forall z \in \mathbb{Z}, z \ge 0 \Rightarrow \mathrm{Irrational}(\sqrt{z}) \iff \lnot \mathrm{IsSquare}(z)$$$

Lean4

theorem irrational_sqrt_intCast_iff_of_nonneg {z : ℤ} (hz : 0 ≤ z) : Irrational (√z) ↔ ¬IsSquare z := by
  rw [← Rat.isSquare_intCast_iff, ← irrational_sqrt_ratCast_iff_of_nonneg (mod_cast hz), Rat.cast_intCast]

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