one_sub_dvd_one_sub_pow

Mathlib.Algebra.Ring.GeomSum

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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