Ideal of ℤ

We prove results about ideals of ℤ or ideals of extensions of ℤ.

In particular, for I an ideal of a ring R extending ℤ, we prove several results about absNorm (under ℤ I) which is the smallest positive integer contained in I.

Main definitions and results

• Int.ideal_span_isMaximal_of_prime: the ideal generated by a prime number is maximal.

• Int.absNorm_under_eq_sInf: the predicate that the absNorm (under ℤ I) is the smallest positive integer in I.

• Int.absNorm_under_dvd_absNorm: absNorm (under ℤ I) divides the norm of I.

instance Int.ideal_span_isMaximal_of_prime (p : ℕ) [Fact (Nat.Prime p)] : (Ideal.span {↑p}).IsMaximal

theorem Int.cast_mem_ideal_iff {R : Type u_1} [Ring R] {I : Ideal R} {d : ℤ} : ↑d ∈ I ↔ ↑(Ideal.absNorm (Ideal.under ℤ I)) ∣ d

theorem Int.absNorm_under_mem {R : Type u_1} [Ring R] (I : Ideal R) : ↑(Ideal.absNorm (Ideal.under ℤ I)) ∈ I

theorem Int.absNorm_under_eq_sInf {R : Type u_1} [Ring R] (I : Ideal R) : Ideal.absNorm (Ideal.under ℤ I) = sInf {d : ℕ | 0 < d ∧ ↑d ∈ I}

theorem Int.absNorm_under_dvd_absNorm {S : Type u_2} [CommRing S] [IsDedekindDomain S] [Module.Free ℤ S] (I : Ideal S) : Ideal.absNorm (Ideal.under ℤ I) ∣ Ideal.absNorm I