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 = 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
    • n.gcd m = (↑n).gcd m,
    Instances For
      def PNat.lcm (n : ℕ+) (m : ℕ+) :

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

      Equations
      • n.lcm m = (↑n).lcm m,
      Instances For
        @[simp]
        theorem PNat.gcd_coe (n : ℕ+) (m : ℕ+) :
        (n.gcd m) = (↑n).gcd m
        @[simp]
        theorem PNat.lcm_coe (n : ℕ+) (m : ℕ+) :
        (n.lcm m) = (↑n).lcm m
        theorem PNat.gcd_dvd_left (n : ℕ+) (m : ℕ+) :
        n.gcd m n
        theorem PNat.gcd_dvd_right (n : ℕ+) (m : ℕ+) :
        n.gcd m m
        theorem PNat.dvd_gcd {m : ℕ+} {n : ℕ+} {k : ℕ+} (hm : k m) (hn : k n) :
        k m.gcd n
        theorem PNat.dvd_lcm_left (n : ℕ+) (m : ℕ+) :
        n n.lcm m
        theorem PNat.dvd_lcm_right (n : ℕ+) (m : ℕ+) :
        m n.lcm m
        theorem PNat.lcm_dvd {m : ℕ+} {n : ℕ+} {k : ℕ+} (hm : m k) (hn : n k) :
        m.lcm n k
        theorem PNat.gcd_mul_lcm (n : ℕ+) (m : ℕ+) :
        n.gcd m * n.lcm 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 : ℕ+} :
          p.Prime1 < p
          instance PNat.instFactPrimeValOfPrime {p : ℕ+} [h : Fact p.Prime] :
          Equations
          • = h
          theorem PNat.dvd_prime {p : ℕ+} {m : ℕ+} (pp : p.Prime) :
          m p m = 1 m = p
          theorem PNat.Prime.ne_one {p : ℕ+} :
          p.Primep 1
          theorem PNat.Prime.not_dvd_one {p : ℕ+} :
          p.Prime¬p 1
          theorem PNat.exists_prime_and_dvd {n : ℕ+} (hn : n 1) :
          ∃ (p : ℕ+), p.Prime p n

          Coprime numbers and gcd #

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

          Two pnats are coprime if their gcd is 1.

          Equations
          • m.Coprime n = (m.gcd n = 1)
          Instances For
            @[simp]
            theorem PNat.coprime_coe {m : ℕ+} {n : ℕ+} :
            (↑m).Coprime n m.Coprime n
            theorem PNat.Coprime.mul {k : ℕ+} {m : ℕ+} {n : ℕ+} :
            m.Coprime kn.Coprime k(m * n).Coprime k
            theorem PNat.Coprime.mul_right {k : ℕ+} {m : ℕ+} {n : ℕ+} :
            k.Coprime mk.Coprime nk.Coprime (m * n)
            theorem PNat.gcd_comm {m : ℕ+} {n : ℕ+} :
            m.gcd n = n.gcd m
            theorem PNat.gcd_eq_left_iff_dvd {m : ℕ+} {n : ℕ+} :
            m n m.gcd n = m
            theorem PNat.gcd_eq_right_iff_dvd {m : ℕ+} {n : ℕ+} :
            m n n.gcd m = m
            theorem PNat.Coprime.gcd_mul_left_cancel (m : ℕ+) {n : ℕ+} {k : ℕ+} :
            k.Coprime n(k * m).gcd n = m.gcd n
            theorem PNat.Coprime.gcd_mul_right_cancel (m : ℕ+) {n : ℕ+} {k : ℕ+} :
            k.Coprime n(m * k).gcd n = m.gcd n
            theorem PNat.Coprime.gcd_mul_left_cancel_right (m : ℕ+) {n : ℕ+} {k : ℕ+} :
            k.Coprime mm.gcd (k * n) = m.gcd n
            theorem PNat.Coprime.gcd_mul_right_cancel_right (m : ℕ+) {n : ℕ+} {k : ℕ+} :
            k.Coprime mm.gcd (n * k) = m.gcd n
            @[simp]
            theorem PNat.one_gcd {n : ℕ+} :
            PNat.gcd 1 n = 1
            @[simp]
            theorem PNat.gcd_one {n : ℕ+} :
            n.gcd 1 = 1
            theorem PNat.Coprime.symm {m : ℕ+} {n : ℕ+} :
            m.Coprime nn.Coprime m
            @[simp]
            @[simp]
            theorem PNat.coprime_one {n : ℕ+} :
            n.Coprime 1
            theorem PNat.Coprime.coprime_dvd_left {m : ℕ+} {k : ℕ+} {n : ℕ+} :
            m kk.Coprime nm.Coprime n
            theorem PNat.Coprime.factor_eq_gcd_left {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : m.Coprime n) (am : a m) (bn : b n) :
            a = (a * b).gcd m
            theorem PNat.Coprime.factor_eq_gcd_right {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : m.Coprime n) (am : a m) (bn : b n) :
            a = (b * a).gcd m
            theorem PNat.Coprime.factor_eq_gcd_left_right {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : m.Coprime n) (am : a m) (bn : b n) :
            a = m.gcd (a * b)
            theorem PNat.Coprime.factor_eq_gcd_right_right {a : ℕ+} {b : ℕ+} {m : ℕ+} {n : ℕ+} (cop : m.Coprime n) (am : a m) (bn : b n) :
            a = m.gcd (b * a)
            theorem PNat.Coprime.gcd_mul (k : ℕ+) {m : ℕ+} {n : ℕ+} (h : m.Coprime n) :
            k.gcd (m * n) = k.gcd m * k.gcd n
            theorem PNat.gcd_eq_left {m : ℕ+} {n : ℕ+} :
            m nm.gcd n = m
            theorem PNat.Coprime.pow {m : ℕ+} {n : ℕ+} (k : ) (l : ) (h : m.Coprime n) :
            (m ^ k).Coprime (n ^ l)