pith. machine review for the scientific record. sign in
theorem proved term proof

coprime_pow_of_prime_not_dvd

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 875theorem coprime_pow_of_prime_not_dvd {p m a : ℕ} (hp : Prime p) (h : ¬p ∣ a) :
 876    Nat.Coprime a (p ^ m) := by

proof body

Term-mode proof.

 877  have hp' : Nat.Prime p := (prime_iff p).1 hp
 878  exact hp'.coprime_pow_of_not_dvd h
 879
 880/-- Two distinct primes raised to powers are coprime. -/

depends on (2)

Lean names referenced from this declaration's body.