noncomputable def IdealNorm.idealNorm {𝒪 : Type u_1} [CommRing 𝒪] (𝔞 : Ideal 𝒪) : ℕ

The (absolute) norm of an ideal 𝔞 of 𝒪, defined as the cardinality of the quotient 𝒪 / 𝔞.

theorem IdealNorm.idealNorm_eq_card_quotient {𝒪 : Type u_1} [CommRing 𝒪] (𝔞 : Ideal 𝒪) : idealNorm 𝔞 = Nat.card (𝒪 ⧸ 𝔞)

The ideal norm equals the cardinality of the quotient ring 𝒪 / 𝔞.

theorem IdealNorm.idealNorm_top {𝒪 : Type u_1} [CommRing 𝒪] : idealNorm ⊤ = 1

The norm of the unit ideal ⊤ is 1.

theorem IdealNorm.idealNorm_bot {𝒪 : Type u_1} [CommRing 𝒪] [Infinite 𝒪] : idealNorm ⊥ = 0

For an infinite ring 𝒪, the norm of the zero ideal ⊥ is 0.

theorem IdealNorm.idealNorm_pos {𝒪 : Type u_2} [CommRing 𝒪] [IsDomain 𝒪] [Module.Free ℤ 𝒪] [Module.Finite ℤ 𝒪] (𝔞 : Ideal 𝒪) (h : 𝔞 ≠ ⊥) : 0 < idealNorm 𝔞

For a nonzero ideal 𝔞 in an integral domain that is a finite free ℤ-module, the ideal norm is strictly positive.

theorem IdealNorm.idealNorm_eq_absNorm {𝒪 : Type u_2} [CommRing 𝒪] [Nontrivial 𝒪] [IsDedekindDomain 𝒪] [Module.Free ℤ 𝒪] (𝔞 : Ideal 𝒪) : Ideal.absNorm 𝔞 = idealNorm 𝔞

For a nontrivial Dedekind domain 𝒪 that is a free ℤ-module, the Mathlib absolute norm Ideal.absNorm agrees with the cardinality-based idealNorm.