card_quotient_toInteger_sub_one — Mathlib

English

The cardinality of the quotient 𝓞_K ⧸ Ideal.span {ζ−1} equals the natAbs of the algebraic norm N_{K/ℚ}(ζ−1).

Русский

Число элементов in 𝓞_K ⧸ Ideal.span {ζ−1} равно |N_{K/ℚ}(ζ−1)|.

LaTeX

$$$$ \operatorname{card} (\mathcal{O}_K / \langle \zeta - 1 \rangle) = \lvert N_{K/\mathbb{Q}}(\zeta - 1) \rvert $$$$

Lean4

/-- We have that `𝓞 K ⧸ Ideal.span {ζ - 1}` has cardinality equal to the norm of `ζ - 1`.

See the results below to compute this norm in various cases. -/
theorem card_quotient_toInteger_sub_one [NumberField K] {k : ℕ} [NeZero k] (hζ : IsPrimitiveRoot ζ k) :
    Nat.card (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) = (Algebra.norm ℤ (hζ.toInteger - 1)).natAbs := by
  rw [← Submodule.cardQuot_apply, ← Ideal.absNorm_apply, Ideal.absNorm_span_singleton]

Похожие утверждения