sub_pow_char_of_commute

Mathlib.Algebra.CharP.Lemmas

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

English

Let R be a ring of characteristic p with p prime. If x and y commute in R, then (x − y)^p = x^p − y^p.

Русский

Пусть R — кольцо с характеристикой p, где p — простое. Если x и y коммутируют, то (x − y)^p = x^p − y^p.

LaTeX

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

Lean4

theorem sub_pow_char_of_commute (h : Commute x y) : (x - y) ^ p = x ^ p - y ^ p :=
  sub_pow_expChar_of_commute _ h

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

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

Разделы

Аффилиация

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