trdeg_lt_aleph0 — Mathlib

English

If R is a domain and S is finite type over R, then trdeg R S is finite; in particular it is less than aleph0.

Русский

Если R — домен и S имеет конечный тип над R, то трансцендентный размер trdeg R S конечен; точнее меньше aleph0.

LaTeX

$$$ [IsDomain R] [fin : Algebra.FiniteType R S] : trdeg R S < \\aleph_0 $$$

Lean4

theorem trdeg_lt_aleph0 [IsDomain R] [fin : FiniteType R S] : trdeg R S < ℵ₀ :=
  have ⟨n, f, surj⟩ := FiniteType.iff_quotient_mvPolynomial''.mp fin
  lift_lt.mp <| (lift_trdeg_le_of_surjective f surj).trans_lt <| by simpa using Cardinal.nat_lt_aleph0 _

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