eight_dvd_sq_sub_one_of_odd

Mathlib.NumberTheory.Multiplicity

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

← MathLib Explorer

English

If k is odd, then 8 divides k^2 − 1.

Русский

Если k нечетно, то 8 делит k^2 − 1.

LaTeX

$$$\text{Odd}(k) \Rightarrow 8 \mid (k^2 - 1).$$$

Lean4

theorem eight_dvd_sq_sub_one_of_odd {k : ℤ} (hk : Odd k) : 8 ∣ k ^ 2 - 1 :=
  by
  rcases hk with ⟨m, rfl⟩
  have eq : (2 * m + 1) ^ 2 - 1 = 4 * (m * (m + 1)) := by ring
  simpa [eq] using (mul_dvd_mul_iff_left four_ne_zero).mpr (two_dvd_mul_add_one m)

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

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

Разделы

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

Аффилиация

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