pow_sub_pow_dvd_pow_sub_pow

Mathlib.Algebra.Ring.GeomSum

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

← MathLib Explorer

English

If m divides k, then x^m − y^m divides x^k − y^k for natural x,y.

Русский

Если m делит k, то x^m − y^m делит x^k − y^k для натуральных x,y.

LaTeX

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

Lean4

theorem pow_sub_pow_dvd_pow_sub_pow (hmk : m ∣ k) : x ^ m - y ^ m ∣ x ^ k - y ^ k := by obtain ⟨n, rfl⟩ := hmk;
  simpa [pow_mul] using (x ^ m).sub_dvd_pow_sub_pow (y ^ m) n

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

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

Разделы

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

Аффилиация

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