isTranscendenceBasis_of_lift_trdeg_le_of_finite

English

If x: ι → A is algebraically independent over R, and the lifted transcendence degree of A over R satisfies lift(trdeg R A) ≤ lift(trdeg ι), then x is a transcendence basis of A over R, in the finite-index setting.

Русский

Пусть x: ι → A алгебраически независимо над R, и приведённый к виду подмножество индексов характер трансцендентности удовлетворяет lift(trdeg R A) ≤ lift(trdeg ι). Тогда x образует базу трансцендентности A над R в случае конечного ι.

LaTeX

$$$\forall {\iota} {x : \iota \to A},\ AlgebraicIndependent R x \to lift(\operatorname{trdeg} R A) \le lift(\#\iota) \to IsTranscendenceBasis R x$$

Lean4

theorem isTranscendenceBasis_of_lift_trdeg_le_of_finite [Finite ι] (hx : AlgebraicIndependent R x)
    (le : lift.{u} (trdeg R A) ≤ lift.{w} #ι) : IsTranscendenceBasis R x :=
  isTranscendenceBasis_of_lift_trdeg_le hx (lift_lt.mp <| le.trans_lt <| by simp) le

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