exists_eq_aeval — Mathlib

English

For nontrivial S and a PowerBasis pb, every y ∈ S can be written as aeval pb.gen f for some f ∈ R[X] with deg bound.

Русский

Для ненулевого S и PowerBasis pb каждый элемент y ∈ S выражается как aeval pb.gen f для некоторого f ∈ R[X] с ограничением deg.

LaTeX

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

Lean4

theorem exists_eq_aeval [Nontrivial S] (pb : PowerBasis R S) (y : S) :
    ∃ f : R[X], f.natDegree < pb.dim ∧ y = aeval pb.gen f :=
  (mem_span_pow pb.dim_ne_zero).mp (by simpa using pb.basis.mem_span y)

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