mvPolynomial' — Mathlib

English

If ι is nonempty, then the corresponding X variables form a transcendence basis.

Русский

Если ι не пусто, соответствующие переменные X образуют базис трансцендентности.

LaTeX

$$$ [Nonempty ι] \Rightarrow IsTranscendenceBasis R (X (R := R) (\sigma := ι))$$$

Lean4

theorem mvPolynomial' [Nonempty ι] : IsTranscendenceBasis R (X (R := R) (σ := ι)) := by nontriviality R;
  exact .mvPolynomial ι R

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