coe_toLinearMap

Mathlib.RingTheory.Bialgebra.Hom

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

English

The application of the toAlgHom coercion to a BialgHom f on a equals f a.

Русский

Применение приведения кAlgHom к BialgHom f на a равно f a.

LaTeX

$$$f.toAlgHom\\;a = f(a)$$$

Lean4

@[simp, norm_cast]
theorem coe_toLinearMap (f : A →ₐc[R] B) : ⇑(f : A →ₗ[R] B) = f :=
  rfl

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

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

Разделы

Аффилиация

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