isTranscendenceBasis_of_le_trdeg — Mathlib

English

If x is an algebraic basis with given le_trdeg, then x is a transcendence basis.

Русский

Если x — базис над R и выполняется ле-трудге, то x — базис трансцендентности.

LaTeX

$$$ (IsDomain A) (x : ι \\to A) (fin : trdeg R A < \\aleph_0) (le : lift.{w} (trdeg R A) \\le lift.{u} #ι) : IsTranscendenceBasis R x $$$

Lean4

theorem isTranscendenceBasis_of_le_trdeg {ι : Type w} (x : ι → A) [Algebra.IsAlgebraic (adjoin R (range x)) A]
    (fin : trdeg R A < ℵ₀) (le : #ι ≤ trdeg R A) : IsTranscendenceBasis R x :=
  isTranscendenceBasis_of_lift_le_trdeg R x fin (by rwa [lift_id, lift_id])

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