lean_workbook_plus_662
ProvedIf both odd then even and odd.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_662 : ∀ a b : ℤ, Odd a ∧ Odd b → Even (a^2 + b^2 + 26) ∧ Odd (5 * a * b) := by sorry
Source
If both odd then even and odd.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_662 : ∀ a b : ℤ, Odd a ∧ Odd b → Even (a^2 + b^2 + 26) ∧ Odd (5 * a * b) := by sorry