irrational_sqrt_intCast_iff — Mathlib

English

For integer z, sqrt(z) is irrational iff z ≥ 0 and z is not a square.

Русский

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

LaTeX

$$$\forall z \in \mathbb{Z}, \mathrm{Irrational}(\sqrt{z}) \iff (\mathrm{IsSquare}(z) \text{ не верно} \land z \ge 0)$$$

Lean4

theorem irrational_sqrt_intCast_iff {z : ℤ} : Irrational (√z) ↔ ¬IsSquare z ∧ 0 ≤ z := by
  rw [← Rat.cast_intCast, irrational_sqrt_ratCast_iff, Rat.isSquare_intCast_iff, Int.cast_nonneg]

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