shiftLeft'_tt_ne_zero

Mathlib.Data.Nat.Size

URI: https://scilib.ai/kg/mathlib#Nat.shiftLeft'_tt_ne_zero

← MathLib Explorer

English

For all n, if n ≠ 0, then shiftLeft' true m n ≠ 0.

Русский

Для всех n, если n ≠ 0, то shiftLeft' true m n ≠ 0.

LaTeX

$$$ \\forall n, n \\neq 0 \\Rightarrow \\operatorname{shiftLeft}'\\, \\text{true} \\, m \\, n \\neq 0 $$$

Lean4

theorem shiftLeft'_tt_ne_zero (m) : ∀ {n}, (n ≠ 0) → shiftLeft' true m n ≠ 0
  | 0, h => absurd rfl h
  | succ _, _ => by dsimp [shiftLeft', bit]; cutsat

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

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

Разделы

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

Аффилиация

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