frobenius_add

Mathlib.Algebra.CharP.Frobenius

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

English

Frobenius preserves addition: frobenius R p (x + y) = frobenius R p x + frobenius R p y.

Русский

Фробениус сохраняет сложение: frobenius (x+y) = frobenius x + frobenius y.

LaTeX

$$$\frobenius R p (x+y) = \frobenius R p x + \frobenius R p y$$$

Lean4

theorem frobenius_add : frobenius R p (x + y) = frobenius R p x + frobenius R p y :=
  (frobenius R p).map_add x y

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

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

Разделы

Аффилиация

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