# Documentation

Mathlib.RingTheory.Int.Basic

# Divisibility over ℕ and ℤ #

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 UniqueFactorizationMonoid instance
• ℤ is a NormalizationMonoid
• ℤ is a GCDMonoid

## Tags #

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

ℕ is a gcd_monoid.

theorem gcd_eq_nat_gcd (m : ) (n : ) :
gcd m n = Nat.gcd m n
theorem lcm_eq_nat_lcm (m : ) (n : ) :
lcm m n = Nat.lcm m n
theorem Int.normUnit_eq (z : ) :
= if 0 z then 1 else -1
theorem Int.normalize_of_nonneg {z : } (h : 0 z) :
normalize z = z
theorem Int.normalize_of_nonpos {z : } (h : z 0) :
normalize z = -z
theorem Int.normalize_coe_nat (n : ) :
normalize n = n
theorem Int.abs_eq_normalize (z : ) :
|z| = normalize z
theorem Int.nonneg_of_normalize_eq_self {z : } (hz : normalize z = z) :
0 z
theorem Int.nonneg_iff_normalize_eq_self (z : ) :
normalize z = z 0 z
theorem Int.eq_of_associated_of_nonneg {a : } {b : } (h : ) (ha : 0 a) (hb : 0 b) :
a = b
theorem Int.coe_gcd (i : ) (j : ) :
↑(Int.gcd i j) = gcd i j
theorem Int.coe_lcm (i : ) (j : ) :
↑(Int.lcm i j) = lcm i j
theorem Int.natAbs_gcd (i : ) (j : ) :
theorem Int.natAbs_lcm (i : ) (j : ) :
theorem Int.exists_unit_of_abs (a : ) :
u x, ↑() = u * a
theorem Int.gcd_eq_natAbs {a : } {b : } :
Int.gcd a b = Nat.gcd () ()
theorem Int.gcd_eq_one_iff_coprime {a : } {b : } :
Int.gcd a b = 1
theorem Int.gcd_ne_one_iff_gcd_mul_right_ne_one {a : } {m : } {n : } :
Int.gcd a (m * n) 1 Int.gcd a m 1 Int.gcd a 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 : Int.gcd a (m * n) = 1) :
Int.gcd a 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 : Int.gcd a (m * n) = 1) :
Int.gcd a n = 1

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

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

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

Instances For
theorem Int.Prime.dvd_mul {m : } {n : } {p : } (hp : ) (h : p m * n) :
p p
theorem Int.Prime.dvd_mul' {m : } {n : } {p : } (hp : ) (h : p m * n) :
p m p n
theorem Int.Prime.dvd_pow {n : } {k : } {p : } (hp : ) (h : p n ^ k) :
p
theorem Int.Prime.dvd_pow' {n : } {k : } {p : } (hp : ) (h : p n ^ k) :
p n
theorem prime_two_or_dvd_of_dvd_two_mul_pow_self_two {m : } {p : } (hp : ) (h : p 2 * m ^ 2) :
p = 2 p
theorem Int.exists_prime_and_dvd {n : } (hn : 1) :
p, p n
theorem Nat.factors_eq {n : } :
theorem Nat.factors_multiset_prod_of_irreducible {s : } (h : ∀ (x : ), x s) :
theorem multiplicity.finite_int_iff {a : } {b : } :
1 b 0
instance multiplicity.decidableNat :
DecidableRel fun a b => ().Dom
instance multiplicity.decidableInt :
DecidableRel fun a b => ().Dom
theorem induction_on_primes {P : } (h₀ : P 0) (h₁ : P 1) (h : (p a : ) → P aP (p * a)) (n : ) :
P n
theorem Int.associated_iff {a : } {b : } :
a = b a = -b
theorem Int.span_natAbs (a : ) :
Ideal.span {↑()} = Ideal.span {a}
theorem Int.eq_pow_of_mul_eq_pow_bit1_left {a : } {b : } {c : } (hab : ) {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 : ) {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 : ) {k : } (h : a * b = c ^ bit1 k) :
(d, a = d ^ bit1 k) e, b = e ^ bit1 k