Theorems · Theorem · number theory
Nat.Prime.pow_eq_iff
∀ {p a k : ℕ}, Nat.Prime p → (a ^ k = p ↔ a = p ∧ k = 1)- Defined in
- Mathlib.Data.Nat.Prime.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.Primestatement and proof · cited by 2,059
- pow_oneproof · cited by 894
- Nat.Prime.eq_one_of_powproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- IsPrimitiveRoot.toInteger_sub_one_dvd_primeproof · cited by 1
- IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_twoproof · cited by 1
- IsPrimitiveRoot.norm_pow_sub_one_eq_prime_pow_of_ne_zeroproof · cited by 1