mathlib
9df3f0d4 - feat(data/nat/prime): nat.prime.eq_pow_iff (#8917)

Commit

4 years ago

feat(data/nat/prime): nat.prime.eq_pow_iff (#8917) If a^k=p then a=p and k=1.

Author

tb65536

tb65536

Parents

Loading