lean_workbook_plus_19387
ProvedIf a number is a multiple of , then it can be written as the product of two even numbers.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_19387 (n : ℕ) (h : n % 4 = 0) : ∃ a b, a % 2 = 0 ∧ b % 2 = 0 ∧ n = a * b := by sorry
Source