coe_restrictScalars

Mathlib.Algebra.Algebra.NonUnitalHom

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

English

The underlying nonunital map of the restricted scalar homomorphism equals the restricted function.

Русский

Подлежащая неединичному отображению карта ограниченного скаляра совпадает с ограниченной функцией.

LaTeX

$$$\\big( f\\restrict_R\\big) : A\\to B=f$$$

Lean4

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

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

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

Разделы

Аффилиация

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