Theorems · Theorem · number theory

NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (n : ℕ),
  Nat.card ↑{I | Submodule.IsPrincipal ↑I ∧ Ideal.absNorm ↑I = n} * NumberField.Units.torsionOrder K =
    Nat.card ↑{a | NumberField.mixedEmbedding.norm ↑a = ↑n}

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.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Cited by

0 results in Mathlib

Foundations

Depth 341 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberField