bodd_coe

Mathlib.Data.Int.Bitwise

URI: https://scilib.ai/kg/mathlib#Int.bodd_coe

English

For any natural n, bodd n equals Nat.bodd n after casting to Int.

Русский

Для любого натурального n bodd n равен Nat.bodd n после приведения к Int.

LaTeX

$$$\\mathrm{bodd}(n) = \\mathrm{Nat}.\\mathrm{bodd}(n)$ for all $n \\in \\mathbb{N}$$$

Lean4

@[simp, norm_cast]
theorem bodd_coe (n : ℕ) : Int.bodd n = Nat.bodd n :=
  rfl

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

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

Разделы

Аффилиация

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