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

instance Nat.instWfDvdMonoidNatToCommMonoidWithZeroLinearOrderedCommMonoidWithZero :

WfDvdMonoid ℕ

Equations

Nat.instWfDvdMonoidNatToCommMonoidWithZeroLinearOrderedCommMonoidWithZero = Nat.instWfDvdMonoidNatToCommMonoidWithZeroLinearOrderedCommMonoidWithZero.proof_1

instance Nat.instUniqueFactorizationMonoidNatCancelCommMonoidWithZero :

UniqueFactorizationMonoid ℕ

Equations

Nat.instUniqueFactorizationMonoidNatCancelCommMonoidWithZero = Nat.instUniqueFactorizationMonoidNatCancelCommMonoidWithZero.proof_1

instance instGCDMonoidNatCancelCommMonoidWithZero :

ℕ 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.instGCDMonoidIntToCancelCommMonoidWithZeroInstCommSemiringIntIsDomainToLinearOrderedRingLinearOrderedCommRing :

Equations

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

instance Int.instNormalizedGCDMonoidIntToCancelCommMonoidWithZeroInstCommSemiringIntIsDomainToLinearOrderedRingLinearOrderedCommRing :

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 x, ↑(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.

Instances For

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 : ℕ), 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