Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-04 15:02 08e1adc8

View on Github →

feat(data/pnat): basic pnat facts needed for perfect numbers (3094) (#3274) define pnat.coprime add some basic lemmas pnats, mostly about coprime, gcd designate some existing lemmas with @[simp]

Estimated changes

added theorem pnat.coe_eq_one_iff
added theorem pnat.coe_inj
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.coprime_coe
added theorem pnat.coprime_one
added theorem pnat.dvd_prime
added theorem pnat.eq_one_of_lt_two
added theorem pnat.gcd_comm
added theorem pnat.gcd_eq_left
added theorem pnat.gcd_one
added theorem pnat.le_of_dvd
added theorem pnat.not_prime_one
added theorem pnat.one_coprime
added theorem pnat.one_gcd
added theorem pnat.prime.ne_one
added theorem pnat.prime.not_dvd_one
added theorem pnat.prime.one_lt
added theorem pnat.prime_two