English
If the base is finite, then RatFunc K is a finite-dimensional extension of RatFunc k, and the finite dimension equals the finite rank of k in K; otherwise, finiteness is characterized by rank comparison with aleph-null.
Русский
Если база конечна, RatFunc K является конечномерным расширением RatFunc k; если нет, конечность определяется через размерности и алеф-подобные пределы.
LaTeX
$$$\text{finrank}_{k} K = \text{finrank}(\text{RatFunc } k, \text{RatFunc } K)$$$
Lean4
theorem finrank_ratFunc_ratFunc : Module.finrank (RatFunc k) (RatFunc K) = Module.finrank k K :=
by
by_cases hf : Module.Finite (RatFunc k) (RatFunc K)
· have hrank := rank_ratFunc_ratFunc k K
rw [← Module.finrank_eq_rank] at hrank
exact (Module.finrank_eq_of_rank_eq hrank.symm).symm
· have hf' : ¬Module.Finite k K := by
rwa [← Module.rank_lt_aleph0_iff, ← rank_ratFunc_ratFunc, Module.rank_lt_aleph0_iff]
rw [Module.finrank_of_not_finite hf, Module.finrank_of_not_finite hf']
