bit_bodd_div2

Mathlib.Data.Nat.Bits

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

English

For all n, bit (bodd(n)) (div2(n)) = n.

Русский

Для всех n, bit(bodd(n))(div2(n)) = n.

LaTeX

$$$\mathrm{bit}(\mathrm{bodd}(n), \mathrm{div2}(n)) = n$$$

Lean4

@[simp, grind =]
theorem bit_bodd_div2 (n : Nat) : bit (bodd n) (div2 n) = n :=
  (bit_val _ _).trans <| (Nat.add_comm _ _).trans <| bodd_add_div2 _

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

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

Разделы

Аффилиация

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