adjoin_singleton_induction — Mathlib

English

If a ∈ adjoin R { x }, then 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

@[elab_as_elim]
theorem _root_.Algebra.adjoin_singleton_induction {M : (adjoin R { x }) → Prop} (a : adjoin R { x })
    (f : ∀ (p : Polynomial R), M (⟨aeval x p, aeval_mem_adjoin_singleton R x⟩ : adjoin R { x })) : M a :=
  by
  obtain ⟨p, hp⟩ := Algebra.adjoin_eq_exists_aeval _ x a
  aesop

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