mathlib3 documentation

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]

def nat.wf_dvd_monoid :

wf_dvd_monoid ℕ

@[protected, instance]

def nat.unique_factorization_monoid :

unique_factorization_monoid ℕ

@[protected, instance]

def nat.gcd_monoid :

ℕ is a gcd_monoid.

Equations

nat.gcd_monoid = {gcd := nat.gcd, lcm := nat.lcm, gcd_dvd_left := nat.gcd_dvd_left, gcd_dvd_right := nat.gcd_dvd_right, dvd_gcd := nat.gcd_monoid._proof_1, gcd_mul_lcm := nat.gcd_monoid._proof_2, lcm_zero_left := nat.lcm_zero_left, lcm_zero_right := nat.lcm_zero_right}

@[protected, instance]

def nat.normalized_gcd_monoid :

normalized_gcd_monoid ℕ

Equations

nat.normalized_gcd_monoid = {to_normalization_monoid := {norm_unit := normalization_monoid.norm_unit infer_instance, norm_unit_zero := nat.normalized_gcd_monoid._proof_1, norm_unit_mul := nat.normalized_gcd_monoid._proof_2, norm_unit_coe_units := nat.normalized_gcd_monoid._proof_3}, to_gcd_monoid := {gcd := gcd_monoid.gcd infer_instance, lcm := gcd_monoid.lcm infer_instance, gcd_dvd_left := nat.normalized_gcd_monoid._proof_4, gcd_dvd_right := nat.normalized_gcd_monoid._proof_5, dvd_gcd := nat.normalized_gcd_monoid._proof_6, gcd_mul_lcm := nat.normalized_gcd_monoid._proof_7, lcm_zero_left := nat.normalized_gcd_monoid._proof_8, lcm_zero_right := nat.normalized_gcd_monoid._proof_9}, normalize_gcd := nat.normalized_gcd_monoid._proof_10, normalize_lcm := nat.normalized_gcd_monoid._proof_11}

theorem gcd_eq_nat_gcd (m n : ℕ) :

gcd_monoid.gcd m n = m.gcd n

theorem lcm_eq_nat_lcm (m n : ℕ) :

gcd_monoid.lcm m n = m.lcm n

@[protected, instance]

def int.normalization_monoid :

normalization_monoid ℤ

Equations

int.normalization_monoid = {norm_unit := λ (a : ℤ), ite (0 ≤ a) 1 (-1), norm_unit_zero := int.normalization_monoid._proof_3, norm_unit_mul := int.normalization_monoid._proof_4, norm_unit_coe_units := int.normalization_monoid._proof_5}

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 : associated a b) (ha : 0 ≤ a) (hb : 0 ≤ b) :

a = b

@[protected, instance]

def int.gcd_monoid :

Equations

int.gcd_monoid = {gcd := λ (a b : ℤ), ↑(a.gcd b), lcm := λ (a b : ℤ), ↑(a.lcm b), gcd_dvd_left := int.gcd_monoid._proof_3, gcd_dvd_right := int.gcd_monoid._proof_4, dvd_gcd := int.gcd_monoid._proof_5, gcd_mul_lcm := int.gcd_monoid._proof_6, lcm_zero_left := int.gcd_monoid._proof_7, lcm_zero_right := int.gcd_monoid._proof_8}

@[protected, instance]

def int.normalized_gcd_monoid :

normalized_gcd_monoid ℤ

Equations

int.normalized_gcd_monoid = {to_normalization_monoid := {norm_unit := normalization_monoid.norm_unit int.normalization_monoid, norm_unit_zero := int.normalized_gcd_monoid._proof_3, norm_unit_mul := int.normalized_gcd_monoid._proof_4, norm_unit_coe_units := int.normalized_gcd_monoid._proof_5}, to_gcd_monoid := {gcd := gcd_monoid.gcd infer_instance, lcm := gcd_monoid.lcm infer_instance, gcd_dvd_left := int.normalized_gcd_monoid._proof_6, gcd_dvd_right := int.normalized_gcd_monoid._proof_7, dvd_gcd := int.normalized_gcd_monoid._proof_8, gcd_mul_lcm := int.normalized_gcd_monoid._proof_9, lcm_zero_left := int.normalized_gcd_monoid._proof_10, lcm_zero_right := int.normalized_gcd_monoid._proof_11}, normalize_gcd := int.normalized_gcd_monoid._proof_12, normalize_lcm := int.normalized_gcd_monoid._proof_13}

theorem int.coe_gcd (i j : ℤ) :

↑(i.gcd j) = gcd_monoid.gcd i j

theorem int.coe_lcm (i j : ℤ) :

↑(i.lcm j) = gcd_monoid.lcm i j

theorem int.nat_abs_gcd (i j : ℤ) :

(gcd_monoid.gcd i j).nat_abs = i.gcd j

theorem int.nat_abs_lcm (i j : ℤ) :

(gcd_monoid.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_nat_abs {a b : ℤ} :

a.gcd b = a.nat_abs.gcd b.nat_abs

theorem int.gcd_eq_one_iff_coprime {a b : ℤ} :

a.gcd b = 1 ↔ is_coprime a b

theorem int.coprime_iff_nat_coprime {a b : ℤ} :

is_coprime a b ↔ a.nat_abs.coprime b.nat_abs

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 : is_coprime a b) (heq : a * b = c ^ 2) :

∃ (a0 : ℤ), a = a0 ^ 2 ∨ a = -a0 ^ 2

theorem int.nat_abs_euclidean_domain_gcd (a b : ℤ) :

(euclidean_domain.gcd a b).nat_abs = a.gcd b

def associates_int_equiv_nat :

associates ℤ ≃ ℕ

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

Equations

associates_int_equiv_nat = {to_fun := λ (z : associates ℤ), z.out.nat_abs, inv_fun := λ (n : ℕ), associates.mk ↑n, left_inv := associates_int_equiv_nat._proof_2, right_inv := associates_int_equiv_nat._proof_3}

theorem int.prime.dvd_mul {m n : ℤ} {p : ℕ} (hp : nat.prime p) (h : ↑p ∣ m * n) :

p ∣ m.nat_abs ∨ p ∣ n.nat_abs

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

theorem int.prime.dvd_pow' {n : ℤ} {k p : ℕ} (hp : nat.prime p) (h : ↑p ∣ n ^ k) :

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 : ℤ), prime p ∧ p ∣ n

theorem nat.factors_eq {n : ℕ} :

unique_factorization_monoid.normalized_factors n = ↑(n.factors)

theorem nat.factors_multiset_prod_of_irreducible {s : multiset ℕ} (h : ∀ (x : ℕ), x ∈ s → irreducible x) :

unique_factorization_monoid.normalized_factors s.prod = s

theorem multiplicity.finite_int_iff_nat_abs_finite {a b : ℤ} :

multiplicity.finite a b ↔ multiplicity.finite a.nat_abs b.nat_abs

theorem multiplicity.finite_int_iff {a b : ℤ} :

multiplicity.finite a b ↔ a.nat_abs ≠ 1 ∧ b ≠ 0

@[protected, instance]

def multiplicity.decidable_nat :

decidable_rel (λ (a b : ℕ), (multiplicity a b).dom)

Equations

multiplicity.decidable_nat = λ (a b : ℕ), decidable_of_iff (a ≠ 1 ∧ 0 < b) _

@[protected, instance]

def multiplicity.decidable_int :

decidable_rel (λ (a b : ℤ), (multiplicity a b).dom)

Equations

multiplicity.decidable_int = λ (a b : ℤ), decidable_of_iff (a.nat_abs ≠ 1 ∧ b ≠ 0) _

theorem induction_on_primes {P : ℕ → Prop} (h₀ : P 0) (h₁ : P 1) (h : ∀ (p a : ℕ), nat.prime p → P a → P (p * a)) (n : ℕ) :

P n

theorem int.associated_nat_abs (k : ℤ) :

associated k ↑(k.nat_abs)

theorem int.prime_iff_nat_abs_prime {k : ℤ} :

prime k ↔ nat.prime k.nat_abs

theorem int.associated_iff_nat_abs {a b : ℤ} :

associated a b ↔ a.nat_abs = b.nat_abs

theorem int.associated_iff {a b : ℤ} :

associated a b ↔ a = b ∨ a = -b

theorem int.zmultiples_nat_abs (a : ℤ) :

add_subgroup.zmultiples ↑(a.nat_abs) = add_subgroup.zmultiples a

theorem int.span_nat_abs (a : ℤ) :

ideal.span {↑(a.nat_abs)} = ideal.span {a}

theorem int.eq_pow_of_mul_eq_pow_bit1_left {a b c : ℤ} (hab : is_coprime a 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 : is_coprime a 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 : is_coprime a b) {k : ℕ} (h : a * b = c ^ bit1 k) :

(∃ (d : ℤ), a = d ^ bit1 k) ∧ ∃ (e : ℤ), b = e ^ bit1 k