sub_pow_char

Mathlib.Algebra.CharP.Lemmas

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

English

In a commutative ring of characteristic p, (x − y)^p = x^p − y^p.

Русский

В коммутативном кольце с характеристикой p выполняется (x − y)^p = x^p − y^p.

LaTeX

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

Lean4

theorem sub_pow_char : (x - y) ^ p = x ^ p - y ^ p :=
  sub_pow_expChar ..

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

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

Разделы

Аффилиация

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