pow_sub_one_dvd_pow_sub_one

Mathlib.Algebra.Ring.GeomSum

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

English

If m divides k, then x^m − 1 divides x^k − 1.

Русский

Если m делит k, то x^m − 1 делит x^k − 1.

LaTeX

$$$$ x^{m} - 1 \mid x^{k} - 1 \quad (m \mid k) $$$$

Lean4

theorem pow_sub_one_dvd_pow_sub_one (hmk : m ∣ k) : x ^ m - 1 ∣ x ^ k - 1 := by
  simpa using pow_sub_pow_dvd_pow_sub_pow x 1 hmk

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

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

Разделы

Аффилиация

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