lean_workbook_plus_15837
ProvedAnyway, In the same way, and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15837 (p q r : ℕ) : p ∣ q * r + q + r → p ∣ p * q + q * r + r * p + p + q + r := by sorry
Source
Anyway, In the same way, and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_15837 (p q r : ℕ) : p ∣ q * r + q + r → p ∣ p * q + q * r + r * p + p + q + r := by sorry