English
For any ideal I in a Dedekind domain S with appropriate structure, absNorm I equals the cardinality of the quotient S/I.
Русский
Для идеала I в области Дедекнда верно, что absNorm I равно-cardQuot(S/I).
LaTeX
$$$[\\text{IsDedekindDomain } S] \\rightarrow \\forall I:\\; absNorm(I) = cardQuot(I)$$$
Lean4
/-- The absolute norm of the ideal `I : Ideal R` is the cardinality of the quotient `R ⧸ I`. -/
noncomputable def absNorm [Nontrivial S] [IsDedekindDomain S] [Module.Free ℤ S] : Ideal S →*₀ ℕ
where
toFun := Submodule.cardQuot
map_mul' I J := by rw [cardQuot_mul]
map_one' := by rw [Ideal.one_eq_top, cardQuot_top]
map_zero' := by
have : Infinite S := Module.Free.infinite ℤ S
rw [Ideal.zero_eq_bot, cardQuot_bot]
