cardinal_le_max_transcendence_basis'

English

For a transcendence basis v over R, the lifted cardinality of K equals the lifted cardinality of the index set ι.

Русский

Для базы трансцендентности v над R выполняется равенство кардиналов после подъема: \\lift #K = \\lift #ι.

LaTeX

$$Cardinal.lift #K = Cardinal.lift #ι$$

Lean4

/-- The cardinality of an algebraically closed `R`-algebra is less than or equal to
the maximum of the cardinality of `R`, the cardinality of a transcendence basis and
`ℵ₀`

A less-universe polymorphic, but simpler statement of
`IsAlgClosed.cardinal_le_max_transcendence_basis` -/
theorem cardinal_le_max_transcendence_basis' (hv : IsTranscendenceBasis R v') : #K' ≤ max (max #R #ι') ℵ₀ := by
  simpa using cardinal_le_max_transcendence_basis v' hv

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