A prime unramified in two number fields is unramified in their compositum

Let $\Omega$ be a field of characteristic zero, let $E_1, E_2 \subseteq \Omega$ be number fields (subfields that are finite over $\mathbb{Q}$), and let $\ell$ be a prime number. Assume that $\ell$ is unramified in $E_1$ and in $E_2$. The statement asserts that $\ell$ is unramified in the compositum:

No Galois hypothesis is necessary.

Proof idea. Local proof: the completion of $E_1 E_2$ at a prime over $\ell$ is the compositum of completions of $E_1$ and $E_2$, and a compositum of unramified extensions of $\mathbb{Q}_\ell$ is unramified. Global proof: after localization at $\ell$, the ring $\mathcal{O}_{E_1} \otimes_{\mathbb{Z}} \mathcal{O}_{E_2}$ is finite étale over $\mathbb{Z}_{(\ell)}$; its image in $E_1 E_2$ is a finite étale domain, hence normal, hence equal to the localized ring of integers of $E_1 E_2$. A third proof for Galois fields uses inertia groups: the inertia group of the compositum embeds in the product of the two inertia groups.

Use. A child of the tame step NumberField.exists_isUnramifiedIn_le_sup_of_prime_ne of the Kronecker-Weber theorem. There it is used for abelian fields only.

Formalization Note. "Unramified" is Algebra.IsUnramifiedIn (𝓞 E) (Ideal.span {(ℓ : ℤ)}), where 𝓞 E is the integral closure of ℤ in E. The compositum is E₁ ⊔ E₂ : IntermediateField ℚ Ω. The hypothesis hℓ is not necessary for the truth of the statement. Mathlib has NumberField.not_dvd_discr_iff_isUnramifiedIn (an integer prime is unramified if and only if it does not divide the discriminant); it has no statement on the discriminant or the ramification of a compositum.