Congruences of integer norms

In a possibly noncommutative ring that is free of finite rank over ℤ, elements congruent modulo (m) have norms congruent modulo m. These are the determinants of left multiplication. This supplies congruences for absolute norms of principal ideals when the integer norms have nonnegative product.

Main results

• Algebra.intCast_norm_eq_of_sub_mem_span_natCast: congruent elements have congruent norms.
• Ideal.span_singleton_natCast_eq_top_iff: in a nontrivial finite free ℤ-algebra, the ideal (m) is the unit ideal exactly when m = 1.

theorem Algebra.intCast_norm_eq_of_sub_mem_span_natCast {S : Type u_1} [Ring S] [Module.Free ℤ S] [Module.Finite ℤ S] {m : ℕ} {a b : S} (h : a - b ∈ Ideal.span {↑m}) : ↑((norm ℤ) a) = ↑((norm ℤ) b)

Congruent elements have congruent norms. If a ≡ b modulo the ideal (m) of a ring S that is free of finite rank over ℤ, then N(a) ≡ N(b) modulo m. Commutativity of S is not required: the norm is the determinant of left multiplication.

theorem Ideal.span_singleton_natCast_eq_top_iff {S : Type u_1} [Ring S] [Module.Free ℤ S] [Module.Finite ℤ S] [Nontrivial S] {m : ℕ} : span {↑m} = ⊤ ↔ m = 1

The ideal (m) is the unit ideal only for m = 1, in a nontrivial ring that is free of finite rank over ℤ. The ring need not be commutative.