Documentation

Mathlib.RingTheory.Int.Basic

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 #

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.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]
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]
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]
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.