lean_workbook_plus_30405
ProvedProve that if is odd, then is odd.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_30405 (n : ℤ) : n^2 % 2 = 1 → n % 2 = 1 := by sorry
Source
Prove that if is odd, then is odd.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_30405 (n : ℤ) : n^2 % 2 = 1 → n % 2 = 1 := by sorry