Ring of integers of ℚ(μ∞): non-Noetherian of dimension 1

Let $K = \mathbb Q(\mu_\infty)$ be the field obtained from $\mathbb Q$ by adjoining all roots of unity (precisely: $K$ is generated over $\mathbb Q$ by roots of unity and contains a primitive $n$-th root of unity for every $n \ge 1$). Let $\mathcal O_K$ be the integral closure of $\mathbb Z$ in $K$. Then

1. $\mathcal O_K$ is not a Noetherian ring, and
2. $\mathcal O_K$ has Krull dimension exactly $1$.

So finite-dimensional affine schemes need not be Noetherian.

Formalization Note The source speaks of a general infinite Galois extension "such as" $\mathbb Q(\mu_\infty)/\mathbb Q$; only this explicit example is formalized, since the claim is not true for every infinite algebraic extension.