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

instance Int.normalizationMonoid : NormalizationMonoid ℤ

Equations

• One or more equations did not get rendered due to their size.

theorem Int.normUnit_eq (z : ℤ) : normUnit 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 : Associated a b) (ha : 0 ≤ a) (hb : 0 ≤ b) : a = b

instance Int.instGCDMonoid : GCDMonoid ℤ

Equations

• One or more equations did not get rendered due to their size.

instance Int.instNormalizedGCDMonoid : NormalizedGCDMonoid ℤ

Equations

• Int.instNormalizedGCDMonoid = let __src := Int.normalizationMonoid; let __src_1 := inferInstance; NormalizedGCDMonoid.mk Int.instNormalizedGCDMonoid.proof_1 Int.instNormalizedGCDMonoid.proof_2

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.natAbs_gcd (i : ℤ) (j : ℤ) : (gcd i j).natAbs = i.gcd j

theorem Int.natAbs_lcm (i : ℤ) (j : ℤ) : (lcm i j).natAbs = i.lcm j

theorem Int.exists_unit_of_abs (a : ℤ) : ∃ (u : ℤ) (_ : IsUnit u), ↑a.natAbs = u * a

theorem Int.gcd_eq_natAbs {a : ℤ} {b : ℤ} : a.gcd b = a.natAbs.gcd b.natAbs

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

def associatesIntEquivNat : Associates ℤ ≃ ℕ

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

Equations

• One or more equations did not get rendered due to their size.

theorem Int.Prime.dvd_mul {m : ℤ} {n : ℤ} {p : ℕ} (hp : p.Prime) (h : ↑p ∣ m * n) : p ∣ m.natAbs ∨ p ∣ n.natAbs

theorem Int.Prime.dvd_mul' {m : ℤ} {n : ℤ} {p : ℕ} (hp : p.Prime) (h : ↑p ∣ m * n) : ↑p ∣ m ∨ ↑p ∣ n

theorem Int.Prime.dvd_pow {n : ℤ} {k : ℕ} {p : ℕ} (hp : p.Prime) (h : ↑p ∣ n ^ k) : p ∣ n.natAbs

theorem Int.Prime.dvd_pow' {n : ℤ} {k : ℕ} {p : ℕ} (hp : p.Prime) (h : ↑p ∣ n ^ k) : ↑p ∣ n

theorem prime_two_or_dvd_of_dvd_two_mul_pow_self_two {m : ℤ} {p : ℕ} (hp : p.Prime) (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.associated_natAbs (k : ℤ) : Associated k ↑k.natAbs

theorem Int.prime_iff_natAbs_prime {k : ℤ} : Prime k ↔ k.natAbs.Prime

theorem Int.associated_iff_natAbs {a : ℤ} {b : ℤ} : Associated a b ↔ a.natAbs = b.natAbs

theorem Int.associated_iff {a : ℤ} {b : ℤ} : Associated a b ↔ a = b ∨ a = -b

theorem Int.zmultiples_natAbs (a : ℤ) : AddSubgroup.zmultiples ↑a.natAbs = AddSubgroup.zmultiples a

theorem Int.span_natAbs (a : ℤ) : Ideal.span {↑a.natAbs} = Ideal.span {a}

theorem Int.eq_pow_of_mul_eq_pow_bit1_left {a : ℤ} {b : ℤ} {c : ℤ} (hab : IsCoprime 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 : IsCoprime 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 : IsCoprime a b) {k : ℕ} (h : a * b = c ^ bit1 k) : (∃ (d : ℤ), a = d ^ bit1 k) ∧ ∃ (e : ℤ), b = e ^ bit1 k