Divisibility over ℤ

This file collects results for the integers that use ring theory in their proofs or cases of ℤ being examples of structures in ring theory.

Main statements

• Int.Prime.dvd_mul': A prime number dividing a product in ℤ divides at least one factor.
• Int.exists_prime_and_dvd: Every non-unit integer has a prime divisor.
• Int.prime_iff_natAbs_prime: Primality in ℤ corresponds to primality of its absolute value in ℕ.
• Int.span_natAbs: The principal ideal generated by a.natAbs is equal to that of a.

Tags

prime, irreducible, integers, normalization monoid, gcd monoid, greatest common divisor

@[deprecated "use `isCoprime_iff_gcd_eq_one.symm` instead" (since := "2025-01-23")]

theorem Int.gcd_eq_one_iff_coprime {a b : ℤ} : a.gcd b = 1 ↔ IsCoprime a b

theorem Int.isCoprime_iff_nat_coprime {a b : ℤ} : IsCoprime a b ↔ a.natAbs.Coprime b.natAbs

@[deprecated Int.isCoprime_iff_nat_coprime (since := "2025-01-23")]

theorem Int.coprime_iff_nat_coprime {a b : ℤ} : IsCoprime a b ↔ a.natAbs.Coprime b.natAbs

Alias of Int.isCoprime_iff_nat_coprime.

theorem Int.gcd_ne_one_iff_gcd_mul_right_ne_one {a : ℤ} {m n : ℕ} : a.gcd (↑m * ↑n) ≠ 1 ↔ a.gcd ↑m ≠ 1 ∨ a.gcd ↑n ≠ 1

If gcd a (m * n) ≠ 1, then gcd a m ≠ 1 or gcd a n ≠ 1.

theorem Int.sq_of_gcd_eq_one {a b c : ℤ} (h : a.gcd b = 1) (heq : a * b = c ^ 2) : ∃ (a0 : ℤ), a = a0 ^ 2 ∨ a = -a0 ^ 2

theorem Int.sq_of_isCoprime {a b c : ℤ} (h : IsCoprime a b) (heq : a * b = c ^ 2) : ∃ (a0 : ℤ), a = a0 ^ 2 ∨ a = -a0 ^ 2

@[deprecated Int.sq_of_isCoprime (since := "2025-01-23")]

theorem Int.sq_of_coprime {a b c : ℤ} (h : IsCoprime a b) (heq : a * b = c ^ 2) : ∃ (a0 : ℤ), a = a0 ^ 2 ∨ a = -a0 ^ 2

Alias of Int.sq_of_isCoprime.

theorem Int.natAbs_euclideanDomain_gcd (a b : ℤ) : (EuclideanDomain.gcd a b).natAbs = a.gcd b

theorem Int.Prime.dvd_mul {m n : ℤ} {p : ℕ} (hp : Nat.Prime p) (h : ↑p ∣ m * n) : p ∣ m.natAbs ∨ p ∣ n.natAbs

theorem Int.Prime.dvd_mul' {m n : ℤ} {p : ℕ} (hp : Nat.Prime p) (h : ↑p ∣ m * n) : ↑p ∣ m ∨ ↑p ∣ n

theorem Int.Prime.dvd_pow {n : ℤ} {k p : ℕ} (hp : Nat.Prime p) (h : ↑p ∣ n ^ k) : p ∣ n.natAbs

theorem Int.Prime.dvd_pow' {n : ℤ} {k p : ℕ} (hp : Nat.Prime p) (h : ↑p ∣ n ^ k) : ↑p ∣ n

theorem prime_two_or_dvd_of_dvd_two_mul_pow_self_two {m : ℤ} {p : ℕ} (hp : Nat.Prime p) (h : ↑p ∣ 2 * m ^ 2) : p = 2 ∨ p ∣ m.natAbs

theorem Int.exists_prime_and_dvd {n : ℤ} (hn : n.natAbs ≠ 1) : ∃ (p : ℤ), Prime p ∧ p ∣ n

theorem Int.prime_iff_natAbs_prime {k : ℤ} : Prime k ↔ Nat.Prime k.natAbs

theorem Int.span_natAbs (a : ℤ) : Ideal.span {↑a.natAbs} = Ideal.span {a}

theorem Int.eq_pow_of_mul_eq_pow_odd_left {a b c : ℤ} (hab : IsCoprime a b) {k : ℕ} (hk : Odd k) (h : a * b = c ^ k) : ∃ (d : ℤ), a = d ^ k

theorem Int.eq_pow_of_mul_eq_pow_odd_right {a b c : ℤ} (hab : IsCoprime a b) {k : ℕ} (hk : Odd k) (h : a * b = c ^ k) : ∃ (d : ℤ), b = d ^ k

theorem Int.eq_pow_of_mul_eq_pow_odd {a b c : ℤ} (hab : IsCoprime a b) {k : ℕ} (hk : Odd k) (h : a * b = c ^ k) : (∃ (d : ℤ), a = d ^ k) ∧ ∃ (e : ℤ), b = e ^ k