mathlib documentation

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

Tags

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

theorem nat.prime_iff {p : } :

@[instance]

Equations
theorem int.normalize_of_nonneg {z : } (h : 0 z) :

theorem int.normalize_of_neg {z : } (h : z < 0) :

@[instance]

Equations
theorem int.coe_gcd (i j : ) :
(i.gcd j) = gcd i j

theorem int.coe_lcm (i j : ) :
(i.lcm j) = lcm i j

theorem int.nat_abs_gcd (i j : ) :
(gcd i j).nat_abs = i.gcd j

theorem int.nat_abs_lcm (i j : ) :
(lcm i 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_one_iff_coprime {a b : } :
a.gcd b = 1 is_coprime a b

theorem int.sqr_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.sqr_of_coprime {a b c : } (h : is_coprime a 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

@[instance]

Equations
@[instance]

Equations