coe_restrictScalars

Mathlib.Algebra.Star.StarAlgHom

URI: https://scilib.ai/kg/mathlib#NonUnitalStarAlgHom.coe_restrictScalars

English

The underlying map of the restricted scalar form equals the original map.

Русский

Базовая функция ограниченного по скалярам вида равна исходной функции.

LaTeX

$$$f.restrictScalars R : A \to B = f$$$

Lean4

theorem coe_restrictScalars (f : A →⋆ₙₐ[S] B) : (f.restrictScalars R : A →ₙ+* B) = f :=
  rfl

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

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

Разделы

Аффилиация

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