nthRoots_two_eq_zero_iff — Mathlib

English

Over a domain, X^2 − r has no roots iff r is not a square.

Русский

В области полином X^2 − r не имеет корней тогда и только тогда, когда r не является квадратом.

LaTeX

$$$\operatorname{nthRoots}(2, r) = 0 \iff \neg \operatorname{IsSquare}(r)$$$

Lean4

@[simp]
theorem nthRoots_two_eq_zero_iff {r : R} : nthRoots 2 r = 0 ↔ ¬IsSquare r := by
  simp_rw [isSquare_iff_exists_sq, eq_zero_iff_forall_notMem, mem_nthRoots (by simp : 0 < 2), ← not_exists, eq_comm]

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