English
For all m,n ∈ ℤ, bodd(mn) equals bodd(m) ∧ bodd(n): the product is odd iff both factors are odd.
Русский
Произведение нечётно тогда, когда оба множителя нечётны: bodd(mn) = bodd(m) ∧ bodd(n).
LaTeX
$$$$ \forall m,n \in \mathbb{Z},\ \operatorname{bodd}(m n) = \operatorname{bodd}(m) \land \operatorname{bodd}(n). $$$$
Lean4
@[simp]
theorem bodd_mul (m n : ℤ) : bodd (m * n) = (bodd m && bodd n) := by
rcases m with m | m <;> rcases n with n | n <;>
simp only [ofNat_eq_coe, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat, negSucc_mul_negSucc] <;>
simp only [negSucc_eq, ← Int.natCast_succ, bodd_neg, bodd_coe, Nat.bodd_mul]
