mul — Mathlib

English

If a and b are odd, then their product ab is odd.

Русский

Если a и b нечётны, то их произведение ab нечётно.

LaTeX

$$$\operatorname{Odd} a \rightarrow \operatorname{Odd} b \rightarrow \operatorname{Odd}(a b)$$$

Lean4

@[simp]
theorem mul : Odd a → Odd b → Odd (a * b) := by
  rintro ⟨a, rfl⟩ ⟨b, rfl⟩
  refine ⟨2 * a * b + b + a, ?_⟩
  rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc, ← Nat.cast_two, ←
    Nat.cast_comm]

Похожие утверждения