sub_pow_expChar_of_commute

Mathlib.Algebra.CharP.Lemmas

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

← MathLib Explorer

English

Let x,y ∈ R commute and p prime with ExpChar R p. Then\n (x - y)^p = x^p - y^p.

Русский

Пусть x,y коммутируют в R и p простое с ExpChar R p. Тогда\n (x - y)^p = x^p - y^p.

LaTeX

$$$(x-y)^p = x^p - y^p$$$

Lean4

theorem sub_pow_expChar_of_commute (h : Commute x y) : (x - y) ^ p = x ^ p - y ^ p := by
  simp [eq_sub_iff_add_eq, ← add_pow_expChar_of_commute _ (h.sub_left rfl)]

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

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

Разделы

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

Аффилиация

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