adjoin_eq_exists_aeval — Mathlib

English

For any a ∈ adjoin R { x }, there exists p with aeval x p = a.

Русский

Для любого a ∈ adjoin R { x } существует p такой что aeval x p = a.

LaTeX

$$$\\exists p: R[X], \\mathrm{aeval}_x(p) = a$$$

Lean4

theorem _root_.Algebra.adjoin_eq_exists_aeval (a : Algebra.adjoin R { x }) : ∃ p : R[X], aeval x p = a :=
  by
  have : (a : A) ∈ Algebra.adjoin R { x } := by simp
  set y := (a : A) with h
  rw [Algebra.adjoin_singleton_eq_range_aeval] at this
  simp_all

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