restrict_mk

Mathlib.RingTheory.Frobenius

URI: https://scilib.ai/kg/mathlib#AlgHom.IsArithFrobAt.restrict_mk

English

On representatives, the restricted Frobenius behaves by mapping x to φ(x): the restriction sends the class of x to the class of φ(x).

Русский

На представительских элементах ограниченный Фробениус действует так: образ класса x равен классу φ(x).

LaTeX

$$$H.restrict(\,\overline{x}\,) = \overline{φ(x)}$$$

Lean4

theorem restrict_mk (x : S) : H.restrict ↑x = ↑(φ x) :=
  rfl

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

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

Разделы

Аффилиация

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