lean_workbook_plus_49909
Provedif ,then
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_49909 (p n : ℕ) (hp : Nat.Prime p) (h : ¬ p ∣ n) : Nat.lcm n (n + p) = n * (n + p) := by sorry
Source
if ,then
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_49909 (p n : ℕ) (hp : Nat.Prime p) (h : ¬ p ∣ n) : Nat.lcm n (n + p) = n * (n + p) := by sorry