Residue field of a prime is finite

Stream: Is there code for X?

[Michail Karatarakis]

Hi, do we have the fact that if $K$ is a number field and $\mathfrak{p}$ is a non-zero prime ideal in $\mathcal{O}_K$, then the residue field $\mathcal{O}_K/\mathfrak{p}$ is finite ?

[Johan Commelin]

cc @Anne Baanen

[Anne Baanen]

I can't think of an explicit statement from the top of my head, but certainly you should be able to cook something up using docs#ideal.rel_hom (which is defined as the cardinality of O_K / p if it's finite, or 0 otherwise).

[Anne Baanen]

Something like: let P be a prime ideal and p ∈ P be a prime integer, then the norm of P divides the norm of p, which is nonzero, so the norm of P is nonzero, so O_K / P is finite. I think we have all the required ingredients.

[Junyan Xu]

You mean docs#ideal.rel_norm, I guess. docs#ideal.factors.inertia_deg_ne_zero seems also relevant.
Once you know $\mathcal{O}_K$ is finite over $\mathbb{Z}$ (e.g. from #18474), then $\mathcal{O}_K/\mathfrak{p}$ is finite over $\mathbb{Z}/\mathfrak{p}\cap\mathbb{Z}$, whose cardinality is a prime number.

[Michail Karatarakis]

OK, thanks a lot.