English
For a given K and n, the product of the number of principal ideals of norm n and the order of torsion equals the cardinality of elements in integerSet of norm n.
Русский
Для данного K и n произведение числа главных идеалов норме n и порядка торов равняется кардиналу множества элементов integerSet(K) норме n.
LaTeX
$$$\\operatorname{card\\_principal\\_norm\\_eq\\_mul\\_torsion}(K,n) : \\operatorname{card}\\{I\\in (\\mathcal{I}(\\mathcal{O}_K))^0 : \\operatorname{IsPrincipal}(I) \\wedge |I|=n \\} \\cdot \\operatorname{torsionOrder}(K) = \\operatorname{card}\\{a:\\; a\\in \\text{integerSet}(K) : \\operatorname{mixedEmbedding.norm}(a)=n\\}.$$$
Lean4
/-- For `n` positive, the number of principal ideals in `𝓞 K` of norm `n` multiplied by the order
of the torsion of `K` is equal to the number of elements in `integerSet K` of norm `n`. -/
theorem card_isPrincipal_norm_eq_mul_torsion (n : ℕ) :
Nat.card {I : (Ideal (𝓞 K))⁰ | IsPrincipal (I : Ideal (𝓞 K)) ∧ absNorm (I : Ideal (𝓞 K)) = n} * torsionOrder K =
Nat.card {a : integerSet K | mixedEmbedding.norm (a : mixedSpace K) = n} :=
by
rw [torsionOrder, ← Nat.card_eq_fintype_card, ← Nat.card_prod]
exact Nat.card_congr (integerSetEquivNorm K n).symm
