rank_eq_cardinalMk — Mathlib

English

For a transcendental extension, the module rank equals the cardinality of the extension.

Русский

Для трансцендентального расширения ранг модуля равен кардиналу расширения.

LaTeX

$$$\\mathrm{Module.rank}\\, F\\, E = \\#E$$$

Lean4

theorem rank_eq_cardinalMk (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.Transcendental F E] :
    Module.rank F E = #E := by
  obtain ⟨ι, x, hx⟩ := exists_isTranscendenceBasis' F E
  haveI := hx.nonempty_iff_transcendental.2 ‹_›
  simpa [← hx.lift_cardinalMk_eq_max_lift] using hx.lift_rank_eq_max_lift

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