transcendental_supported_X_iff — Mathlib

English

[Nontrivial R] The transcendence of X_i over (supported R s) is equivalent to i ∉ s.

Русский

[Не тривиальный R] Трансцендентность X_i над (supported R s) эквивалентна i ∉ s.

LaTeX

$$$$ [\text{Nontrivial } R] \Rightarrow (\text{Transcendental} (X_i : MvPolynomial \sigma R) \text{ over } \text{supported } R s) \iff i \notin s. $$$$

Lean4

theorem transcendental_supported_X_iff [Nontrivial R] {i : σ} {s : Set σ} :
    Transcendental (supported R s) (X i : MvPolynomial σ R) ↔ i ∉ s := by
  simpa [Polynomial.transcendental_X] using
    transcendental_supported_polynomial_aeval_X_iff R (i := i) (s := s) (f := Polynomial.X)

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