# mathlib3documentation

ring_theory.int.basic

# Divisibility over ℕ and ℤ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main statements #

• nat.factors_eq: the multiset of elements of nat.factors is equal to the factors given by the unique_factorization_monoid instance
• ℤ is a normalization_monoid
• ℤ is a gcd_monoid

## Tags #

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

@[protected, instance]
@[protected, instance]
@[protected, instance]

ℕ is a gcd_monoid.

Equations
@[protected, instance]
Equations
theorem gcd_eq_nat_gcd (m n : ) :
= m.gcd n
theorem lcm_eq_nat_lcm (m n : ) :
= m.lcm n
@[protected, instance]
Equations
theorem int.normalize_of_nonneg {z : } (h : 0 z) :
= z
theorem int.normalize_of_nonpos {z : } (h : z 0) :
= -z
theorem int.normalize_coe_nat (n : ) :
theorem int.abs_eq_normalize (z : ) :
theorem int.nonneg_of_normalize_eq_self {z : } (hz : = z) :
0 z
theorem int.eq_of_associated_of_nonneg {a b : } (h : b) (ha : 0 a) (hb : 0 b) :
a = b
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem int.coe_gcd (i j : ) :
(i.gcd j) =
theorem int.coe_lcm (i j : ) :
(i.lcm j) =
theorem int.nat_abs_gcd (i j : ) :
j).nat_abs = i.gcd j
theorem int.nat_abs_lcm (i j : ) :
j).nat_abs = i.lcm j
theorem int.exists_unit_of_abs (a : ) :
(u : ) (h : is_unit u), (a.nat_abs) = u * a
theorem int.gcd_eq_nat_abs {a b : } :
theorem int.gcd_eq_one_iff_coprime {a b : } :
a.gcd b = 1 b
theorem int.coprime_iff_nat_coprime {a b : } :
b
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.gcd_eq_one_of_gcd_mul_right_eq_one_left {a : } {m n : } (h : a.gcd (m * n) = 1) :
a.gcd m = 1

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

theorem int.gcd_eq_one_of_gcd_mul_right_eq_one_right {a : } {m n : } (h : a.gcd (m * n) = 1) :
a.gcd n = 1

If gcd a (m * n) = 1, then 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 : b) (heq : a * b = c ^ 2) :
(a0 : ), a = a0 ^ 2 a = -a0 ^ 2

Maps an associate class of integers consisting of -n, n to n : ℕ

Equations
theorem int.prime.dvd_mul {m n : } {p : } (hp : nat.prime p) (h : p m * n) :
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) :
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.nat_abs
theorem int.exists_prime_and_dvd {n : } (hn : n.nat_abs 1) :
(p : ), p n
theorem nat.factors_eq {n : } :
@[protected, instance]
def multiplicity.decidable_nat  :
decidable_rel (λ (a b : ), b).dom)
Equations
@[protected, instance]
def multiplicity.decidable_int  :
decidable_rel (λ (a b : ), b).dom)
Equations
theorem induction_on_primes {P : Prop} (h₀ : P 0) (h₁ : P 1) (h : (p a : ), P a P (p * a)) (n : ) :
P n
theorem int.associated_iff {a b : } :
b a = b a = -b
theorem int.zmultiples_nat_abs (a : ) :
theorem int.eq_pow_of_mul_eq_pow_bit1_left {a b c : } (hab : b) {k : } (h : a * b = c ^ bit1 k) :
(d : ), a = d ^ bit1 k
theorem int.eq_pow_of_mul_eq_pow_bit1_right {a b c : } (hab : b) {k : } (h : a * b = c ^ bit1 k) :
(d : ), b = d ^ bit1 k
theorem int.eq_pow_of_mul_eq_pow_bit1 {a b c : } (hab : b) {k : } (h : a * b = c ^ bit1 k) :
( (d : ), a = d ^ bit1 k) (e : ), b = e ^ bit1 k