Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-27 23:05 0a721ccc

View on Github →

feat(data/nat): a predicate for prime powers (#11313) Adds a predicate for prime powers, in preparation for defining the von Mangoldt function. cc @stuart-presnell since you might be needing this material soon, and @jcommelin if you have thoughts about generalising this to rings/UFDs?

Estimated changes

added theorem eq_of_prime_pow_eq'
added theorem eq_of_prime_pow_eq
added theorem is_prime_pow.dvd
added theorem is_prime_pow.ne_one
added theorem is_prime_pow.ne_zero
added theorem is_prime_pow.one_lt
added theorem is_prime_pow.pos
added theorem is_prime_pow.pow
added theorem is_prime_pow.two_le
added def is_prime_pow
added theorem is_prime_pow_def
added theorem is_prime_pow_nat_iff
added theorem not_is_prime_pow_one
added theorem not_is_prime_pow_zero
added theorem prime.is_prime_pow