trdeg_of_isDomain — Mathlib

English

The transcendence degree of a polynomial ring over S on a set ι is the lift of the cardinality of ι.

Русский

Трансцендентный размер многочленов на множество ι над R равен апгрейдированному кардиналу множества ι.

LaTeX

$$$ trdeg\\; S\\; (MvPolynomial\\; ι\\; S) = \\mathrm{lift}.#ι $$$

Lean4

@[simp]
theorem trdeg_of_isDomain [IsDomain S] : trdeg S (MvPolynomial ι S) = lift.{v} #ι :=
  by
  have := (IsTranscendenceBasis.mvPolynomial ι S).lift_cardinalMk_eq_trdeg.symm
  rwa [lift_id', ← lift_lift.{u}, lift_id] at this

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