frobenius_sub

Mathlib.Algebra.CharP.Frobenius

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

English

For all x,y ∈ R, φ_R,p(x − y) = φ_R,p(x) − φ_R,p(y).

Русский

Для любых x,y ∈ R выполняется φ_R,p(x − y) = φ_R,p(x) − φ_R,p(y).

LaTeX

$$$\operatorname{frobenius}(R,p)(x - y) = \operatorname{frobenius}(R,p)(x) - \operatorname{frobenius}(R,p)(y)$$$

Lean4

theorem frobenius_sub : frobenius R p (x - y) = frobenius R p x - frobenius R p y :=
  map_sub ..

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

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

Разделы

Аффилиация

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