lean_workbook_plus_30088
ProvedA/Q both odd. must be even.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_30088 : ∀ n m : ℤ, Odd n ∧ Odd m → Even (n - m) := by sorry
Source
A/Q both odd. must be even.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_30088 : ∀ n m : ℤ, Odd n ∧ Odd m → Even (n - m) := by sorry