lean_workbook_plus_15777
ProvedIf and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15777 : ∀ n : ℕ, n ≡ 0 [ZMOD 3] → ∃ x : ℕ, n = 3 * x := by sorry
Source
If and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_15777 : ∀ n : ℕ, n ≡ 0 [ZMOD 3] → ∃ x : ℕ, n = 3 * x := by sorry