lean_workbook_plus_61497
ProvedIf is prime and then prove that or
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61497 (p : ℕ) (b c : ℕ) (hp : p.Prime) (h : p ∣ b * c) : p ∣ b ∨ p ∣ c := by sorry
Source
If is prime and then prove that or
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_61497 (p : ℕ) (b c : ℕ) (hp : p.Prime) (h : p ∣ b * c) : p ∣ b ∨ p ∣ c := by sorry