cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt'

English

If K' is uncountable and algebraically closed, then its cardinality equals the cardinality of a transcendence basis when compared with a nontrivial base ring.

Русский

Если K' не счетно и алгебраически замкнуто, то кардинал K' равен кардиналу трансцендентной базы относительно некоторой базовой кольцо.

LaTeX

$$cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt$$

Lean4

/-- If `K` is an uncountable algebraically closed field, then its
cardinality is the same as that of a transcendence basis.

This is a simpler, but less general statement of
`cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt`. -/
theorem cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt' [Nontrivial R] (hv : IsTranscendenceBasis R v')
    (hR : #R ≤ ℵ₀) (hK : ℵ₀ < #K') : #K' = #ι' := by
  simpa using cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt v' hv hR hK

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