Equal unit ranks in an extension: $K$ totally real, $L/K$ totally complex quadratic

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted this Lean statement, at the explicit request of the account owner. Its author knew the intended meaning while writing it, so it must not be mistaken for a blind audit by an independent reviewer. Please compare it against the Lean code itself.

Throughout, $K$ is a number field (a field of characteristic zero that is finite-dimensional over $\mathbb Q$), $\mathcal O_K$ is its ring of integers and $\mathcal O_K^\times$ the unit group. $r_1$ denotes the number of real infinite places of $K$ and $r_2$ the number of complex infinite places (each complex place corresponds to a pair of complex-conjugate embeddings $K\to\mathbb C$). Statement. Let $K$ and $L$ be number fields (possibly in different universes) and let $L$ be a $K$-algebra (so $K\to L$ is a field embedding), with $1 < [L:K]$ where $[L:K]$ is Mathlib's Module.finrank K L (this is $0$ if $L$ were infinite-dimensional over $K$, so the hypothesis forces finite dimension). Then: the finite rank of $\mathcal O_L^\times$ equals the finite rank of $\mathcal O_K^\times$ if and only if all of: $K$ is totally real, $L$ is totally complex, and $[L:K]=2$.

Here the finite rank of an abelian group is Module.finrank ℤ of its additive version: the rank as a natural number when that rank is finite, and $0$ by convention when the rank is infinite.