Lemmas related to Nat.Prime and lcm

This file contains lemmas related to Nat.Prime. These lemmas are kept separate from Mathlib/Data/Nat/GCD/Basic.lean in order to minimize imports.

Main results

• Nat.Prime.dvd_or_dvd_of_dvd_lcm: If p ∣ lcm a b, then p ∣ a ∨ p ∣ b.
• Nat.Prime.dvd_lcm: p ∣ lcm a b ↔ p ∣ a ∨ p ∣ b.
• Nat.Prime.not_dvd_lcm: If p ∤ a and p ∤ b, then p ∤ lcm a b.

theorem Nat.Prime.dvd_or_dvd_of_dvd_lcm {p a b : ℕ} (hp : Prime p) (h : p ∣ a.lcm b) : p ∣ a ∨ p ∣ b

theorem Nat.Prime.dvd_lcm {p a b : ℕ} (hp : Prime p) : p ∣ a.lcm b ↔ p ∣ a ∨ p ∣ b

theorem Nat.Prime.not_dvd_lcm {p a b : ℕ} (hp : Prime p) (ha : ¬p ∣ a) (hb : ¬p ∣ b) : ¬p ∣ a.lcm b