Divisors of a Natural Power

Stream: maths

[Colin Jones ⚛️]

Is there a theorem for this?

example (h : 0 ≤ k ∧ k ≤ n ∧ p ^ k ≠ a) (hp : Prime p)  : ¬ a ∣ p ^ n := by
  obtain ⟨h1, ⟨h2, h3⟩⟩ := h
  sorry

Essentially, I'm saying that only p ^ 1, p ^ 2, ..., p^ n can divide p ^ n if p is Prime.

[Damiano Testa]

Is docs#Nat.dvd_prime_pow close enough?

[Colin Jones ⚛️]

Thank you that's good enough

[Yury G. Kudryashov]

Note that the exampl you formulated lacks a \forall or \exists on k.