cardinalMk_le_trdeg — Mathlib

English

If x is algebraically independent over R, mk ι ≤ trdeg R A.

Русский

Если x алгебраически независим над R, то кардинал mk ι не превосходит трансцендентную степень над R.

LaTeX

$$$\\operatorname{AlgIndep}_R x \\Rightarrow \\lvert \\iota \\rvert \\le \\operatorname{trdeg} R A$$$

Lean4

theorem cardinalMk_le_trdeg [Nontrivial R] {ι : Type v} {x : ι → A} (hx : AlgebraicIndependent R x) : #ι ≤ trdeg R A :=
  by rw [← (#ι).lift_id, ← (trdeg R A).lift_id]; exact hx.lift_cardinalMk_le_trdeg

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