irrational_sqrt_ratCast_iff — Mathlib

English

For any rational q, sqrt(q) is irrational iff not IsSquare q and q ≥ 0.

Русский

Для любого рационала q sqrt(q) иррационально тогда и только тогда, когда q не является квадратом и q≥0.

LaTeX

$$$\forall q \in \mathbb{Q}, \mathrm{Irrational}(\sqrt{q}) \iff (\lnot \mathrm{IsSquare}(q) \\land q \ge 0)$$$

Lean4

theorem irrational_sqrt_ratCast_iff {q : ℚ} : Irrational (√q) ↔ ¬IsSquare q ∧ 0 ≤ q :=
  by
  obtain hq | hq := le_or_gt 0 q
  · simp_rw [irrational_sqrt_ratCast_iff_of_nonneg hq, and_iff_left hq]
  · rw [sqrt_eq_zero_of_nonpos (Rat.cast_nonpos.2 hq.le)]
    simp_rw [not_irrational_zero, false_iff, not_and, not_le, hq, implies_true]

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