exists_eq_aeval' — Mathlib

English

Even without explicit degree bound, y can be written as aeval pb.gen f for some f ∈ R[X].

Русский

Без явного ограничения по степени существует f ∈ R[X] так, что y = aeval pb.gen f.

LaTeX

$$$\\exists f : R[X], y = aeval pb.gen f$.$$

Lean4

theorem exists_eq_aeval' (pb : PowerBasis R S) (y : S) : ∃ f : R[X], y = aeval pb.gen f :=
  by
  nontriviality S
  obtain ⟨f, _, hf⟩ := exists_eq_aeval pb y
  exact ⟨f, hf⟩

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