isTranscendenceBasis_of_trdeg_le_of_finite

English

If ι is finite and x: ι → A is algebraically independent over R with trdeg_R A ≤ #ι, then x is a transcendence basis of A over R.

Русский

Если ι конечен и x: ι → A алгебраически независим над R, и trdeg_R A ≤ #ι, то x образует базу трансцендентности A над R.

LaTeX

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

Lean4

theorem isTranscendenceBasis_of_trdeg_le_of_finite {ι : Type w} [Finite ι] {x : ι → A} (hx : AlgebraicIndependent R x)
    (le : trdeg R A ≤ #ι) : IsTranscendenceBasis R x :=
  isTranscendenceBasis_of_lift_trdeg_le_of_finite hx (by rwa [lift_id, lift_id])

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