rootSet — Mathlib

English

The set of distinct roots equals the finset of roots collected from the multiset of roots.

Русский

Множество различных корней равно конечному сету корней, полученному из мультиса корней.

LaTeX

$$$$ \mathrm{rootSet}(p,S) = (\mathrm{aroots}(p,S)).\text{toFinset} $$$$

Lean4

/-- The set of distinct roots of `p` in `S`.

If you have a non-separable polynomial, use `Polynomial.aroots` for the multiset
where multiple roots have the appropriate multiplicity. -/
def rootSet (p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] : Set S :=
  haveI := Classical.decEq S
  (p.aroots S).toFinset

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