aroots_def — Mathlib

English

An element a is a root of p over S iff p.map(algebraMap T S) ≠ 0 and aeval a p = 0.

Русский

Элемент a является корнем p над S тогда и только тогда, когда p.map(algebraMap T S) ≠ 0 и aeval a p = 0.

LaTeX

$$$a ∈ p.aroots S ↔ p.map (algebraMap T S) ≠ 0 ∧ aeval a p = 0$$$

Lean4

theorem aroots_def (p : T[X]) (S) [CommRing S] [IsDomain S] [Algebra T S] :
    p.aroots S = (p.map (algebraMap T S)).roots :=
  rfl

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