Norms of algebraic integers

The norm N(α) = Algebra.norm ℚ α of a nonzero algebraic integer α is a nonzero integer, so 1 ≤ |N(α)|. The norm of a rational integer m is m ^ [K : ℚ], so divisibility between rational integers is the same in 𝓞 K as in ℤ; in particular 𝓞 K / n 𝓞 K has characteristic n.

Main results

• NumberField.RingOfIntegers.one_le_abs_norm: 1 ≤ |N(α)| for every nonzero α : 𝓞 K.
• NumberField.RingOfIntegers.dvd_natAbs_norm: every α : 𝓞 K divides |N(α)|.
• NumberField.RingOfIntegers.intCast_dvd_intCast: (m : 𝓞 K) ∣ n ↔ m ∣ n for m n : ℤ.
• NumberField.RingOfIntegers.natCast_dvd_natCast: (m : 𝓞 K) ∣ n ↔ m ∣ n for m n : ℕ.
• NumberField.RingOfIntegers.charP_quotient_span_natCast: 𝓞 K / n 𝓞 K has characteristic n.

theorem NumberField.RingOfIntegers.one_le_abs_norm {K : Type u_1} [Field K] [NumberField K] {α : RingOfIntegers K} (hα : α ≠ 0) : 1 ≤ |↑((Algebra.norm ℚ) ↑α)|

The absolute value of the norm of a nonzero algebraic integer is at least one.

theorem NumberField.RingOfIntegers.dvd_natAbs_norm {K : Type u_1} [Field K] [NumberField K] (α : RingOfIntegers K) : α ∣ ↑((Algebra.norm ℤ) α).natAbs

An element α of 𝓞 K divides the absolute value of its norm.

@[simp]

theorem NumberField.RingOfIntegers.intCast_dvd_intCast {K : Type u_1} [Field K] [NumberField K] {m n : ℤ} : ↑m ∣ ↑n ↔ m ∣ n

Divisibility between rational integers is the same in 𝓞 K as in ℤ.

@[simp]

theorem NumberField.RingOfIntegers.natCast_dvd_natCast {K : Type u_1} [Field K] [NumberField K] {m n : ℕ} : ↑m ∣ ↑n ↔ m ∣ n

Divisibility between natural numbers is the same in 𝓞 K as in ℕ.

instance NumberField.RingOfIntegers.charP_quotient_span_natCast (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : CharP (RingOfIntegers K ⧸ Ideal.span {↑n}) n

The residue ring 𝓞 K / n 𝓞 K has characteristic n.