lean_workbook_plus_33870
ProvedProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_33870 {m n : ℤ} (hm : m % 2 = 1) (hn : n % 2 = 1) : (m * n) % 2 = 1 := by sorrySource
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_33870 {m n : ℤ} (hm : m % 2 = 1) (hn : n % 2 = 1) : (m * n) % 2 = 1 := by sorry