The constants of ℂ(x) over ℝ

The rational function field ℂ(x) is a function field over ℝ, but its full constant field is ℂ. Consequently its zero-divisor Riemann–Roch space has real dimension two. This concrete example shows why the equality ℓ(0) = 1 requires the exact-constants hypothesis.

@[simp]

theorem TauCeti.Divisor.dim_zero_real_ratFunc_complex : dim 0 = 2

The zero-divisor Riemann–Roch space of ℂ(x) has real dimension two.