Divisibility over ℕ and ℤ

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

Main statements

• Nat.factors_eq: the multiset of elements of Nat.factors is equal to the factors given by the UniqueFactorizationMonoid instance

Tags

prime, irreducible, natural numbers, integers, normalization monoid, gcd monoid, greatest common divisor, prime factorization, prime factors, unique factorization, unique factors

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

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

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_coprime {a b c : ℤ} (h : IsCoprime a b) (heq : a * b = c ^ 2) : ∃ (a0 : ℤ), a = a0 ^ 2 ∨ a = -a0 ^ 2

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.zmultiples_natAbs (a : ℤ) : AddSubgroup.zmultiples ↑a.natAbs = AddSubgroup.zmultiples a

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

@[deprecated Int.eq_pow_of_mul_eq_pow_odd_left (since := "2024-07-12")]

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

Alias of Int.eq_pow_of_mul_eq_pow_odd_left.

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

@[deprecated Int.eq_pow_of_mul_eq_pow_odd_right (since := "2024-07-12")]

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

Alias of Int.eq_pow_of_mul_eq_pow_odd_right.

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

@[deprecated Int.eq_pow_of_mul_eq_pow_odd (since := "2024-07-12")]

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

Alias of Int.eq_pow_of_mul_eq_pow_odd.