algebraicIndependent_X — Mathlib

English

The indeterminates X in the polynomial ring MvPolynomial are algebraically independent over any R.

Русский

Непривязанные переменные X в кольце многочленов MvPolynomial алгебраически независимы над любым R.

LaTeX

$$$\\\\mathrm{AlgebraicIndependent}(R, MvPolynomial.X)$$$

Lean4

theorem algebraicIndependent_X (σ R : Type*) [CommRing R] : AlgebraicIndependent R (X (R := R) (σ := σ)) :=
  by
  rw [AlgebraicIndependent, aeval_X_left]
  exact injective_id

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