polynomial — Mathlib

English

If ι is nonempty and ι is a singleton, the X variable set forms a transcendence basis for the polynomial ring in one variable over R.

Русский

Если ι непуст и единичен, множество переменных X образует базис трансцендентности для многочлена в одну переменную над R.

LaTeX

$$$ [Nonempty ι] [Subsingleton ι] : IsTranscendenceBasis R (fun _ => X)$$$

Lean4

theorem polynomial [Nonempty ι] [Subsingleton ι] : IsTranscendenceBasis R fun _ : ι ↦ (.X : Polynomial R) :=
  by
  nontriviality R
  have := (nonempty_unique ι).some
  refine
    (isTranscendenceBasis_equiv (Equiv.equivPUnit.{_, 1} _).symm).mp <|
      (MvPolynomial.pUnitAlgEquiv R).symm.isTranscendenceBasis_iff.mp ?_
  convert IsTranscendenceBasis.mvPolynomial PUnit R
  ext; simp

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