mem_rootSet' — Mathlib

English

Membership in rootSet' is equivalent to p.map(algebraMap) ≠ 0 and aeval(a) p = 0.

Русский

Принадлежность к rootSet' эквивалентна тому, что p.map(a) ≠ 0 и aeval(a) p = 0.

LaTeX

$$$$ a \in p.rootSet S \;\iff\; p.map(\text{algebraMap}_{T \to S}) \neq 0 \; \land\; \operatorname{aeval}(a,p) = 0 $$$$

Lean4

theorem mem_rootSet' {p : T[X]} {S : Type*} [CommRing S] [IsDomain S] [Algebra T S] {a : S} :
    a ∈ p.rootSet S ↔ p.map (algebraMap T S) ≠ 0 ∧ aeval a p = 0 := by
  classical rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']

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