mod_two_of_bodd

Mathlib.Data.Nat.Bits

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

← MathLib Explorer

English

n mod 2 equals (bodd(n)).toNat.

Русский

n mod 2 равно (bodd(n)).toNat.

LaTeX

$$$n \bmod 2 = (\mathrm{bodd}(n)).\mathrm{toNat}$$$

Lean4

theorem mod_two_of_bodd (n : ℕ) : n % 2 = (bodd n).toNat :=
  by
  have : (n % 2).bodd = n.bodd := by simpa using congr_arg bodd (mod_add_div n 2)
  rw [← this]
  rcases mod_two_eq_zero_or_one n with h | h <;> rw [h] <;> rfl

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

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

Разделы

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

Аффилиация

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