Condition_for_Divisibility_of_Powers_of_Prime
Provedprime-numbersproofwiki
For a prime p and positive integers k, l: p^k | p^l iff k ≤ l.
Preamble
import Mathlib.Data.Nat.Prime.Basic
Formal statement
theorem Condition_for_Divisibility_of_Powers_of_Prime (p : ℕ) (hp : Nat.Prime p) (k l : ℕ) : p ^ k ∣ p ^ l ↔ k ≤ l := by sorry
Source