aroots — Mathlib

English

aroots p S is defined as the multiset of roots of p viewed over S.

Русский

aroots p S определяется как мультикое корней p, рассмотренное как над S.

LaTeX

$$$p.aroots S = (p.map (algebraMap T S)).roots$$$

Lean4

/-- Given a polynomial `p` with coefficients in a ring `T` and a `T`-algebra `S`, `aroots p S` is
the multiset of roots of `p` regarded as a polynomial over `S`. -/
noncomputable abbrev aroots (p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] : Multiset S :=
  (p.map (algebraMap T S)).roots

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