pow_one_sub_dvd_pow_mul_sub_one

Mathlib.Algebra.Ring.GeomSum

URI: https://scilib.ai/kg/mathlib#pow_one_sub_dvd_pow_mul_sub_one

English

For any ring R and any x, integers m,n ≥ 1, x^m − 1 divides x^{mn} − 1.

Русский

Для кольца R и любого x справедливо: x^m − 1 делит x^{mn} − 1.

LaTeX

$$$\\displaystyle x^m - 1 \\;|\\; x^{mn} - 1$$$

Lean4

theorem pow_one_sub_dvd_pow_mul_sub_one (x : R) (m n : ℕ) : x ^ m - 1 ∣ x ^ (m * n) - 1 := by rw [pow_mul];
  exact sub_one_dvd_pow_sub_one (x ^ m) n

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

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

Разделы

Аффилиация

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