English
Every polynomial p ∈ MvPolynomial σ R arises as a rename of some polynomial q for a finite set s ⊆ σ; i.e. there exist s finite and q ∈ MvPolynomial { x // x ∈ s } R with p = rename (↑) q.
Русский
Каждый многочлен p ∈ MvPolynomial σ R получается как переименование некоторого q для конечного множества s ⊆ σ, то есть существуют конечное s и q ∈ MvPolynomial { x // x ∈ s } R such that p = rename (↑) q.
LaTeX
$$$ \exists s\;\exists q\;\; p = rename (\uparrow)\ q \;\text{with } s \text{ finite}$$$
Lean4
/-- Every polynomial is a polynomial in finitely many variables. -/
theorem exists_finset_rename (p : MvPolynomial σ R) :
∃ (s : Finset σ) (q : MvPolynomial { x // x ∈ s } R), p = rename (↑) q := by
classical
apply induction_on p
· intro r
exact ⟨∅, C r, by rw [rename_C]⟩
· rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩
refine ⟨s ∪ t, ⟨?_, ?_⟩⟩
·
refine rename (Subtype.map id ?_) p + rename (Subtype.map id ?_) q <;>
simp +contextual only [id, true_or, or_true, Finset.mem_union, forall_true_iff]
· simp only [rename_rename, map_add]
rfl
· rintro p n ⟨s, p, rfl⟩
refine ⟨insert n s, ⟨?_, ?_⟩⟩
· refine rename (Subtype.map id ?_) p * X ⟨n, s.mem_insert_self n⟩
simp +contextual only [id, or_true, Finset.mem_insert, forall_true_iff]
· simp only [rename_rename, rename_X, map_mul]
rfl
