p m : ℕ+
pp : Prime p
⊢ ↑m ∣ ↑p ↔ m = 1 ∨ m = p
p m : ℕ+
pp : Prime p
⊢ m ∣ p ↔ m = 1 ∨ m = p
rw [PNat.dvd_iff]
p m : ℕ+
pp : Prime p
⊢ ↑m = 1 ∨ ↑m = ↑p ↔ m = 1 ∨ m = p
p m : ℕ+
pp : Prime p
⊢ ↑m ∣ ↑p ↔ m = 1 ∨ m = p
rw [Nat.dvd_prime pp]
no goals
p m : ℕ+
pp : Prime p
⊢ ↑m = 1 ∨ ↑m = ↑p ↔ m = 1 ∨ m = p
simp