cardinalMk_eq_trdeg — Mathlib

English

If x,y are transcendence bases over R, then their index set cardinalities are equal: #ι = #ι'.

Русский

Если x и y — базисы трансцендентности над R, то кардиналы их индексов равны: #ι = #ι'.

LaTeX

$$$ (IsTranscendenceBasis R x) \\rightarrow (IsTranscendenceBasis R y) \\rightarrow \\#ι = \\#ι' $$$

Lean4

theorem cardinalMk_eq_trdeg {ι : Type w} {x : ι → A} (hx : IsTranscendenceBasis R x) : #ι = trdeg R A := by
  rw [← lift_id #ι, lift_cardinalMk_eq_trdeg hx, lift_id]

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