bit_add

Mathlib.Data.Nat.Bits

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

← MathLib Explorer

English

For all b, n, m: bit b (n + m) = bit false n + bit b m.

Русский

Для всех b, n, m: bit b (n + m) = bit false n + bit b m.

LaTeX

$$$$ \forall (b : \mathrm{Bool}) (n,m : \mathbb{N}), \; \mathrm{bit}(b, n + m) = \mathrm{bit}(\mathrm{false}, n) + \mathrm{bit}(b, m). $$$$

Lean4

theorem bit_add : ∀ (b : Bool) (n m : ℕ), bit b (n + m) = bit false n + bit b m
  | true, _, _ => by dsimp [bit]; cutsat
  | false, _, _ => by dsimp [bit]; cutsat

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

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

Разделы

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

Аффилиация

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