Cyclotomic Euler system relations

Throughout, $\zeta = (\zeta_n)$ is a compatible system of roots of unity in $\mathbb C$: for every square-free positive integer $n$, $\zeta_n$ is a primitive $n$-th root of unity, and $\zeta_{mn} = \zeta_m\zeta_n$ whenever $m,n$ are coprime square-free positive integers. Write $\alpha_n = 1-\zeta_n$ and $\mathbb Q(\zeta_n)\subseteq\mathbb C$ for the $n$-th cyclotomic field.

Let $n$ be square-free and $l$ a prime with $l\nmid n$. Then the cyclotomic units satisfy the two Euler-system relations:

1. (Norm relation) If $n>1$ and $\mathrm{Fr}_l$ is the automorphism of $\mathbb Q(\zeta_n)/\mathbb Q$ with $\mathrm{Fr}_l(\zeta_n)=\zeta_n^{\,l}$, then

2. (Congruence relation) For every prime ideal $\mathfrak P$ of the ring of integers of $\mathbb Q(\zeta_{nl})$ lying above $l$,

These two relations are what make $(\alpha_n)_n$ an Euler system; they are the input to Kolyvagin's and Rubin's Euler-system arguments bounding ideal class groups.

Formalization Note The base field of the norm is $\mathbb Q(\zeta_n)$ (the source's $\mathbb Q(\zeta_l)$ is a typo), and $n>1$ is required in the norm relation because $\alpha_1=0$. See the two milestone statements for the encoding details.