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 Nat.instWfDvdMonoidNatToCommMonoidWithZeroLinearOrderedCommMonoidWithZero : WfDvdMonoid ℕ

Equations

• Nat.instWfDvdMonoidNatToCommMonoidWithZeroLinearOrderedCommMonoidWithZero = (_ : WfDvdMonoid ℕ)

instance Nat.instUniqueFactorizationMonoidNatCancelCommMonoidWithZero : UniqueFactorizationMonoid ℕ

Equations

• Nat.instUniqueFactorizationMonoidNatCancelCommMonoidWithZero = (_ : UniqueFactorizationMonoid ℕ)

instance instGCDMonoidNatCancelCommMonoidWithZero : GCDMonoid ℕ

ℕ is a gcd_monoid.

Equations

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

instance instNormalizedGCDMonoidNatCancelCommMonoidWithZero : NormalizedGCDMonoid ℕ

Equations

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

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

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.instGCDMonoidIntToCancelCommMonoidWithZeroInstCommSemiringIntIsDomainToLinearOrderedSemiringToLinearOrderedCommSemiringLinearOrderedCommRingExistsAddOfLEInstAddGroupIntToLEToPreorderToPartialOrderToStrictOrderedSemiring : GCDMonoid ℤ

Equations

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

instance Int.instNormalizedGCDMonoidIntToCancelCommMonoidWithZeroInstCommSemiringIntIsDomainToLinearOrderedSemiringToLinearOrderedCommSemiringLinearOrderedCommRingExistsAddOfLEInstAddGroupIntToLEToPreorderToPartialOrderToStrictOrderedSemiring : NormalizedGCDMonoid ℤ

Equations

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

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

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

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

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

theorem Int.gcd_eq_one_iff_coprime {a : ℤ} {b : ℤ} : Int.gcd a b = 1 ↔ IsCoprime a b

theorem Int.coprime_iff_nat_coprime {a : ℤ} {b : ℤ} : IsCoprime a b ↔ Nat.Coprime (Int.natAbs a) (Int.natAbs b)

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 : IsCoprime a b) (heq : a * b = c ^ 2) : ∃ (a0 : ℤ), a = a0 ^ 2 ∨ a = -a0 ^ 2

theorem Int.natAbs_euclideanDomain_gcd (a : ℤ) (b : ℤ) : Int.natAbs (EuclideanDomain.gcd a b) = Int.gcd a 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 : Nat.Prime p) (h : ↑p ∣ m * n) : p ∣ Int.natAbs m ∨ p ∣ Int.natAbs 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) : p ∣ Int.natAbs n

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 ∣ Int.natAbs m

theorem Int.exists_prime_and_dvd {n : ℤ} (hn : Int.natAbs n ≠ 1) : ∃ (p : ℤ), Prime p ∧ p ∣ n

theorem Nat.factors_eq {n : ℕ} : UniqueFactorizationMonoid.normalizedFactors n = ↑(Nat.factors n)

theorem Nat.factors_multiset_prod_of_irreducible {s : Multiset ℕ} (h : ∀ x ∈ s, Irreducible x) : UniqueFactorizationMonoid.normalizedFactors (Multiset.prod s) = s

theorem multiplicity.finite_int_iff_natAbs_finite {a : ℤ} {b : ℤ} : multiplicity.Finite a b ↔ multiplicity.Finite (Int.natAbs a) (Int.natAbs b)

theorem multiplicity.finite_int_iff {a : ℤ} {b : ℤ} : multiplicity.Finite a b ↔ Int.natAbs a ≠ 1 ∧ b ≠ 0

instance multiplicity.decidableNat : DecidableRel fun (a b : ℕ) => (multiplicity a b).Dom

Equations

• multiplicity.decidableNat x✝ x = decidable_of_iff (x✝ ≠ 1 ∧ 0 < x) (_ : x✝ ≠ 1 ∧ 0 < x ↔ multiplicity.Finite x✝ x)

instance multiplicity.decidableInt : DecidableRel fun (a b : ℤ) => (multiplicity a b).Dom

Equations

• multiplicity.decidableInt x✝ x = decidable_of_iff (Int.natAbs x✝ ≠ 1 ∧ x ≠ 0) (_ : Int.natAbs x✝ ≠ 1 ∧ x ≠ 0 ↔ multiplicity.Finite x✝ x)

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_natAbs (k : ℤ) : Associated k ↑(Int.natAbs k)

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

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

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

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

theorem Int.span_natAbs (a : ℤ) : Ideal.span {↑(Int.natAbs a)} = 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