roots_def — Mathlib

English

The roots of a polynomial p are defined by p.roots, which equals ∅ if p = 0, and otherwise equals a canonical choice from exists_multiset_roots.

Русский

Корни многочлена p задаются как p.roots: если p = 0, то ⌀; иначе — выбранное из exists_multiset_roots множество корней.

LaTeX

$$p.roots = if h : p = 0 then ∅ else Classical.choose (exists_multiset_roots h).$$

Lean4

theorem roots_def [DecidableEq R] (p : R[X]) [Decidable (p = 0)] :
    p.roots = if h : p = 0 then ∅ else Classical.choose (exists_multiset_roots h) :=
  by
  rename_i iR ip0
  obtain rfl := Subsingleton.elim iR (Classical.decEq R)
  obtain rfl := Subsingleton.elim ip0 (Classical.dec (p = 0))
  rfl

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