sub_one_dvd_pow_sub_one

Mathlib.Algebra.Ring.GeomSum

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

← MathLib Explorer

English

For any ring R and any x, x − 1 divides x^n − 1 for all natural n.

Русский

Для любого кольца R и любого x выполняется: x − 1 делит x^n − 1 для всех n.

LaTeX

$$$\\displaystyle x - 1 \\;|\\; x^n - 1$$$

Lean4

theorem sub_one_dvd_pow_sub_one (x : R) (n : ℕ) : x - 1 ∣ x ^ n - 1 :=
  by
  conv_rhs => rw [← one_pow n]
  exact (Commute.one_right x).sub_dvd_pow_sub_pow n

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

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

Разделы

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

Аффилиация

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