isTranscendenceBasis_of_trdeg_le — Mathlib

English

Let R be a nontrivial commutative ring, A an R-algebra with no zero divisors. If x: ι → A is algebraically independent over R and trdeg_R A is finite and at most |ι|, then x is a transcendence basis for A over R.

Русский

Пусть R — ненулевой коммутативный кольцо, A — алгебра над R с нулевыми делителями отсутствующими. Пусть x: ι → A алгебраически независима над R, и числo трансцендентности trdeg_R(A) конечно и не превосходит |ι|. Тогда x образует базу трансцендентности для A над R.

LaTeX

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

Lean4

theorem isTranscendenceBasis_of_trdeg_le {ι : Type w} {x : ι → A} (hx : AlgebraicIndependent R x) (fin : trdeg R A < ℵ₀)
    (le : trdeg R A ≤ #ι) : IsTranscendenceBasis R x :=
  isTranscendenceBasis_of_lift_trdeg_le hx fin (by rwa [lift_id, lift_id])

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