Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-01 21:03 894fb0c5

View on Github →

feat(data/nat/totient): totient_prime_pow (#8353)

Estimated changes

Modified src/data/nat/gcd.lean

added theorem nat.coprime_pow_left_iff

added theorem nat.coprime_pow_right_iff

Modified src/data/nat/totient.lean

added theorem nat.totient_eq_card_coprime

added theorem nat.totient_one

added theorem nat.totient_prime

added theorem nat.totient_prime_pow

added theorem nat.totient_prime_pow_succ

added theorem nat.totient_two