Documentation

Mathlib.Data.PNat.Prime

Primality and GCD on pnat #

This file extends the theory of ℕ+ with gcd, lcm and Prime functions, analogous to those on Nat.

The canonical map from Nat.Primes to ℕ+

Equations
  • p = { val := p, property := (_ : 0 < p) }
Instances For
    theorem Nat.Primes.coe_pnat_nat (p : Nat.Primes) :
    p = p
    theorem Nat.Primes.coe_pnat_inj (p : Nat.Primes) (q : Nat.Primes) :
    p = q p = q
    def PNat.gcd (n : ℕ+) (m : ℕ+) :

    The greatest common divisor (gcd) of two positive natural numbers, viewed as positive natural number.

    Equations
    Instances For
      def PNat.lcm (n : ℕ+) (m : ℕ+) :

      The least common multiple (lcm) of two positive natural numbers, viewed as positive natural number.

      Equations
      Instances For
        @[simp]
        theorem PNat.gcd_coe (n : ℕ+) (m : ℕ+) :
        ↑(PNat.gcd n m) = Nat.gcd n m
        @[simp]
        theorem PNat.lcm_coe (n : ℕ+) (m : ℕ+) :
        ↑(PNat.lcm n m) = Nat.lcm n m
        theorem PNat.gcd_dvd_left (n : ℕ+) (m : ℕ+) :
        theorem PNat.gcd_dvd_right (n : ℕ+) (m : ℕ+) :
        theorem PNat.dvd_gcd {m : ℕ+} {n : ℕ+} {k : ℕ+} (hm : k m) (hn : k n) :
        theorem PNat.dvd_lcm_left (n : ℕ+) (m : ℕ+) :
        theorem PNat.dvd_lcm_right (n : ℕ+) (m : ℕ+) :
        theorem PNat.lcm_dvd {m : ℕ+} {n : ℕ+} {k : ℕ+} (hm : m k) (hn : n k) :
        theorem PNat.gcd_mul_lcm (n : ℕ+) (m : ℕ+) :
        PNat.gcd n m * PNat.lcm n m = n * m
        theorem PNat.eq_one_of_lt_two {n : ℕ+} :
        n < 2n = 1

        Prime numbers #

        def PNat.Prime (p : ℕ+) :

        Primality predicate for ℕ+, defined in terms of Nat.Prime.

        Equations
        Instances For
          theorem PNat.Prime.one_lt {p : ℕ+} :
          PNat.Prime p1 < p
          theorem PNat.dvd_prime {p : ℕ+} {m : ℕ+} (pp : PNat.Prime p) :
          m p m = 1 m = p
          theorem PNat.Prime.ne_one {p : ℕ+} :
          PNat.Prime pp 1
          theorem PNat.exists_prime_and_dvd {n : ℕ+} (hn : n 1) :
          p, PNat.Prime p p n

          Coprime numbers and gcd #

          def PNat.Coprime (m : ℕ+) (n : ℕ+) :

          Two pnats are coprime if their gcd is 1.

          Equations
          Instances For
            @[simp]
            theorem PNat.coprime_coe {m : ℕ+} {n : ℕ+} :
            theorem PNat.Coprime.mul {k : ℕ+} {m : ℕ+} {n : ℕ+} :
            PNat.Coprime m kPNat.Coprime n kPNat.Coprime (m * n) k
            theorem PNat.Coprime.mul_right {k : ℕ+} {m : ℕ+} {n : ℕ+} :
            PNat.Coprime k mPNat.Coprime k nPNat.Coprime k (m * n)
            theorem PNat.gcd_comm {m : ℕ+} {n : ℕ+} :
            theorem PNat.gcd_eq_left_iff_dvd {m : ℕ+} {n : ℕ+} :
            m n PNat.gcd m n = m
            theorem PNat.gcd_eq_right_iff_dvd {m : ℕ+} {n : ℕ+} :
            m n PNat.gcd n m = m
            theorem PNat.Coprime.gcd_mul_left_cancel (m : ℕ+) {n : ℕ+} {k : ℕ+} :
            PNat.Coprime k nPNat.gcd (k * m) n = PNat.gcd m n
            theorem PNat.Coprime.gcd_mul_right_cancel (m : ℕ+) {n : ℕ+} {k : ℕ+} :
            PNat.Coprime k nPNat.gcd (m * k) n = PNat.gcd m n
            @[simp]
            theorem PNat.one_gcd {n : ℕ+} :
            PNat.gcd 1 n = 1
            @[simp]
            theorem PNat.gcd_one {n : ℕ+} :
            PNat.gcd n 1 = 1
            theorem PNat.Coprime.symm {m : ℕ+} {n : ℕ+} :
            @[simp]
            @[simp]
            theorem PNat.Coprime.coprime_dvd_left {m : ℕ+} {k : ℕ+} {n : ℕ+} :
            m kPNat.Coprime k nPNat.Coprime m n
            theorem PNat.Coprime.factor_eq_gcd_left {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : PNat.Coprime m n) (am : a m) (bn : b n) :
            a = PNat.gcd (a * b) m
            theorem PNat.Coprime.factor_eq_gcd_right {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : PNat.Coprime m n) (am : a m) (bn : b n) :
            a = PNat.gcd (b * a) m
            theorem PNat.Coprime.factor_eq_gcd_left_right {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : PNat.Coprime m n) (am : a m) (bn : b n) :
            a = PNat.gcd m (a * b)
            theorem PNat.Coprime.factor_eq_gcd_right_right {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : PNat.Coprime m n) (am : a m) (bn : b n) :
            a = PNat.gcd m (b * a)
            theorem PNat.Coprime.gcd_mul (k : ℕ+) {m : ℕ+} {n : ℕ+} (h : PNat.Coprime m n) :
            PNat.gcd k (m * n) = PNat.gcd k m * PNat.gcd k n
            theorem PNat.gcd_eq_left {m : ℕ+} {n : ℕ+} :
            m nPNat.gcd m n = m
            theorem PNat.Coprime.pow {m : ℕ+} {n : ℕ+} (k : ) (l : ) (h : PNat.Coprime m n) :
            Nat.Coprime (m ^ k) (n ^ l)