irrational_sqrt_ratCast_iff_of_nonneg

English

For nonnegative rational q, irrationality of sqrt(q) is equivalent to q not being a square in ℚ.

Русский

Для неотрицательного рационала q иррациональность sqrt(q) эквивалентна тому, что q не является квадратом в ℚ.

LaTeX

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

Lean4

theorem irrational_sqrt_ratCast_iff_of_nonneg {q : ℚ} (hq : 0 ≤ q) : Irrational (√q) ↔ ¬IsSquare q :=
  by
  refine Iff.not (?_ : Exists _ ↔ Exists _)
  constructor
  · rintro ⟨y, hy⟩
    refine ⟨y, Rat.cast_injective (α := ℝ) ?_⟩
    rw [Rat.cast_mul, hy, mul_self_sqrt (Rat.cast_nonneg.2 hq)]
  · rintro ⟨q', rfl⟩
    exact ⟨|q'|, mod_cast (sqrt_mul_self_eq_abs q').symm⟩

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