isTranscendenceBasis_of_le_trdeg_of_finite

English

For a finite index set ι and an algebraic adjoin over A, if the trdeg is finite and le holds, then x is a transcendence basis.

Русский

Для конечного множества индексов и алгебраического над adjoin_R range x, если трансцендентный размер конечен и выполняется условие le, то x — базис трансцендентности.

LaTeX

$$$ [Finite ι] (x : ι \\to A) [Algebra.IsAlgebraic (adjoin R (Set.range x)) A] (le : lift.{w} (trdeg R A) \\geq ? ) : IsTranscendenceBasis R x $$$

Lean4

theorem isTranscendenceBasis_of_le_trdeg_of_finite {ι : Type w} [Finite ι] (x : ι → A)
    [Algebra.IsAlgebraic (adjoin R (range x)) A] (le : #ι ≤ trdeg R A) : IsTranscendenceBasis R x :=
  isTranscendenceBasis_of_lift_le_trdeg_of_finite R x (by rwa [lift_id, lift_id])

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