Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-26 19:37 e2905697

View on Github →

feat(data/nat/totient): add nat.totient_prime_iff (#8833)

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.filter_card_eq

added theorem finset.not_subset

Modified src/data/nat/prime.lean

added theorem nat.prime_of_coprime

Modified src/data/nat/totient.lean

added theorem nat.totient_eq_iff_prime