lean_workbook_plus_10951
ProvedIf the square of an integer is divisible by , then it is also divisible by . Hence, it follows that and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10951 : ∀ y : ℤ, y^2 % 8 = 0 → y^2 % 16 = 0 := by sorry
Source