rank_ratFunc_ratFunc — Mathlib

English

For algebraic base fields k ⊂ K, the rank of RatFunc K as a RatFunc k-vector space equals the rank of k in K, i.e., the ratio of vector space dimensions matches the algebraic rank of the extension.

Русский

При алгебраическом включении ранк RatFunc K по отношению к RatFunc k равен ранку поля K по отношению к k.

LaTeX

$$$\operatorname{rank}_{k} K = \operatorname{rank}(\text{RatFunc } k, \text{RatFunc } K)$$$

Lean4

theorem rank_ratFunc_ratFunc : Module.rank (RatFunc k) (RatFunc K) = Module.rank k K := by
  rw [Algebra.IsAlgebraic.rank_of_isFractionRing k[X] (RatFunc k) K[X] (RatFunc K), rank_polynomial_polynomial]

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