Commit 2023-01-04 15:04 f5f206c6

View on Github →

feat: port Data.PNat.Primes (#1270) I added a coercion from Nat to PNat. At some point Nat.coprime in Std should be renamed to Nat.Coprime

Estimated changes

added theorem PNat.Coprime.gcd_mul
added theorem PNat.Coprime.mul
added theorem PNat.Coprime.mul_right
added theorem PNat.Coprime.pow
added theorem PNat.Coprime.symm
added def PNat.Coprime
added theorem PNat.Prime.ne_one
added theorem PNat.Prime.not_dvd_one
added theorem PNat.Prime.one_lt
added def PNat.Prime
added theorem PNat.coprime_coe
added theorem PNat.coprime_one
added theorem PNat.dvd_gcd
added theorem PNat.dvd_lcm_left
added theorem PNat.dvd_lcm_right
added theorem PNat.dvd_prime
added theorem PNat.eq_one_of_lt_two
added def PNat.gcd
added theorem PNat.gcd_coe
added theorem PNat.gcd_comm
added theorem PNat.gcd_dvd_left
added theorem PNat.gcd_dvd_right
added theorem PNat.gcd_eq_left
added theorem PNat.gcd_mul_lcm
added theorem PNat.gcd_one
added def PNat.lcm
added theorem PNat.lcm_coe
added theorem PNat.lcm_dvd
added theorem PNat.not_prime_one
added theorem PNat.one_coprime
added theorem PNat.one_gcd
added theorem PNat.prime_two