An even number leaves remainder zero

Exercise · double_mod_two

An even number leaves remainder zero: $2n \bmod 2 = 0$ .

Formal statement · Lean 4.lean

theorem double_mod_two (n : Nat) : (2 * n) % 2 = 0 := by
  sorry

Proof. sorry

Nobody has tried yet.