lean_workbook_plus_77574
ProvedProve that and implies .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_77574 (n : ℕ) (h₁ : n ≡ 0 [ZMOD 2]) (h₂ : 5 ∣ n) : 10 ∣ n := by sorry
Source
Prove that and implies .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_77574 (n : ℕ) (h₁ : n ≡ 0 [ZMOD 2]) (h₂ : 5 ∣ n) : 10 ∣ n := by sorry