coe_toAlgHom

Mathlib.RingTheory.Bialgebra.Hom

URI: https://scilib.ai/kg/mathlib#BialgHom.coe_toAlgHom

English

The underlying LinearMap of a BialgHom when viewed as a LinearMap is equal to the map itself.

Русский

Базовое линейное отображение BialgHom, когда рассматривается как LinearMap, равно самой карте f.

LaTeX

$$$f.toLinearMap = f$$$

Lean4

@[norm_cast]
theorem coe_toAlgHom (f : A →ₐc[R] B) : ⇑(f : A →ₐ[R] B) = f :=
  rfl

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

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

Разделы

Аффилиация

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