mvPolynomial — Mathlib

English

The set of indeterminates X for the multivariate polynomial ring in an index set ι forms a transcendence basis over R.

Русский

Набор неопределённых переменных X для многочлена векторной переменной образует базис трансцендентности над R.

LaTeX

$$$ IsTranscendenceBasis R (X (R := R) (\sigma := ι))$$$

Lean4

theorem mvPolynomial [Nontrivial R] : IsTranscendenceBasis R (X (R := R) (σ := ι)) :=
  by
  refine isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic.2 ⟨algebraicIndependent_X .., ?_⟩
  rw [adjoin_range_X]
  set A := MvPolynomial ι R
  have := Algebra.isIntegral_of_surjective (R := (⊤ : Subalgebra R A)) (B := A) (⟨⟨·, ⟨⟩⟩, rfl⟩)
  infer_instance

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