size_shiftLeft

Mathlib.Data.Nat.Size

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

← MathLib Explorer

English

Let m, n ∈ ℕ with m ≠ 0. Then size (m <<< n) = size m + n.

Русский

Пусть m ∈ ℕ, m ≠ 0 и n ∈ ℕ. Тогда size(m <<< n) = size(m) + n.

LaTeX

$$$m \neq 0 \Rightarrow \operatorname{size}(m \\!\\<<< n) = \operatorname{size}(m) + n$$$

Lean4

@[simp]
theorem size_shiftLeft {m} (h : m ≠ 0) (n) : size (m <<< n) = size m + n := by
  simp only [size_shiftLeft' (shiftLeft'_ne_zero_left _ h _), ← shiftLeft'_false]

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

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

Разделы

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

Аффилиация

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