bodd_mul

Mathlib.Data.Nat.Bits

URI: https://scilib.ai/kg/mathlib#Nat.bodd_mul

← MathLib Explorer

English

bodd(m·n) = bodd(m) ∧ bodd(n).

Русский

bodd(m·n) = bodd(m) и bodd(n).

LaTeX

$$$\mathrm{bodd}(m \cdot n) = \mathrm{bodd}(m) \land \mathrm{bodd}(n)$$$

Lean4

@[simp]
theorem bodd_mul (m n : ℕ) : bodd (m * n) = (bodd m && bodd n) := by
  induction n with
  | zero => simp
  | succ n IH =>
    simp only [mul_succ, bodd_add, IH, bodd_succ]
    cases bodd m <;> cases bodd n <;> rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru