mem_aroots' — Mathlib

English

Under appropriate hypotheses, a ∈ p.aroots S iff p ≠ 0 and aeval a p = 0.

Русский

При подходящих предпосылках, a ∈ p.aroots S тогда и только тогда, когда p ≠ 0 и aeval a p = 0.

LaTeX

$$a ∈ p.aroots S ↔ p ≠ 0 ∧ aeval a p = 0$$

Lean4

theorem mem_aroots' [CommRing S] [IsDomain S] [Algebra T S] {p : T[X]} {a : S} :
    a ∈ p.aroots S ↔ p.map (algebraMap T S) ≠ 0 ∧ aeval a p = 0 := by
  rw [mem_roots', IsRoot.def, ← eval₂_eq_eval_map, aeval_def]

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