nthRoots_two_one — Mathlib

English

The multiset nthRoots 2 1 consists of { -1, 1 }

Русский

Мультимножество nthRoots 2 1 состоит из { -1, 1 }.

LaTeX

$$$\operatorname{nthRoots}(2, 1) = \{-1, 1\}$$$

Lean4

theorem nthRoots_two_one : Polynomial.nthRoots 2 (1 : R) = {-1, 1} :=
  by
  have h₁ : (X ^ 2 - C 1 : R[X]) = (X + C 1) * (X - C 1) := by simp [← sq_sub_sq]
  have h₂ : (X ^ 2 - C 1 : R[X]) ≠ 0 := fun h ↦ by simpa using congrArg (coeff · 0) h
  rw [nthRoots, h₁, roots_mul (h₁ ▸ h₂), roots_X_add_C, roots_X_sub_C]; rfl

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