transcendental_supported_X — Mathlib

English

If i ∉ s, then X_i is transcendental over the subalgebra supported on s.

Русский

Если i не принадлежит s, то X_i трансцендентален над подалгеброй, поддерживаемой на s.

LaTeX

$$$$ i \notin s \implies \text{Transcendental} (\text{X}_i : \text{MvPolynomial } \sigma R) \text{ in } (\text{supported } R s). $$$$

Lean4

theorem transcendental_supported_X {i : σ} {s : Set σ} (h : i ∉ s) :
    Transcendental (supported R s) (X i : MvPolynomial σ R) := by
  simpa using transcendental_supported_polynomial_aeval_X R h (Polynomial.transcendental_X R)

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