English
There exists a finite n and an injective f: Fin n → σ and q ∈ MvPolynomial (Fin n) R such that p = rename f q.
Русский
Существует конечное число n и инъективное отображение f: Fin n → σ и q ∈ MvPolynomial (Fin n) R such that p = rename f q.
LaTeX
$$$ \exists n\;\exists f:\mathrm{Fin}\ n \to\sigma\;\exists q:\mathrm{MvPolynomial} (\mathrm{Fin}\ n) R,\; p = rename f q $$$
Lean4
/-- Every polynomial is a polynomial in finitely many variables. -/
theorem exists_fin_rename (p : MvPolynomial σ R) :
∃ (n : ℕ) (f : Fin n → σ) (_hf : Injective f) (q : MvPolynomial (Fin n) R), p = rename f q :=
by
obtain ⟨s, q, rfl⟩ := exists_finset_rename p
let n := Fintype.card { x // x ∈ s }
let e := Fintype.equivFin { x // x ∈ s }
refine ⟨n, (↑) ∘ e.symm, Subtype.val_injective.comp e.symm.injective, rename e q, ?_⟩
rw [← rename_rename, rename_rename e]
simp only [Function.comp_def, Equiv.symm_apply_apply, rename_rename]
