transcendental_adjoin_iff — Mathlib

English

If hx: x is algebraically independent over R, then for any set s and i ∉ s, the element x_i is transcendental over the adjoin R (x '' s).

Русский

Если x алгебраически независим над R, то для любого множества s и элемента i не принадлежащего s, x_i трансцендентно над adjoin_R( x'' s ).

LaTeX

$$$\\mathrm{Transcendental}\\big(\\mathrm{adjoin}_R(x''s),\; x_i\\big) \\text{ если } i \\notin s$$$

Lean4

theorem transcendental_adjoin_iff [Nontrivial A] {s : Set ι} {i : ι} :
    Transcendental (adjoin R (x '' s)) (x i) ↔ i ∉ s :=
  by
  rw [← Set.disjoint_singleton_right]
  convert ← hx.adjoin_iff_disjoint (t := { i })
  rw [algebraicIndependent_singleton_iff ⟨i, rfl⟩]

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