coe_toAddHom

Mathlib.Algebra.Module.LinearMap.Defs

URI: https://scilib.ai/kg/mathlib#LinearMap.coe_toAddHom

English

The underlying function of f.toAddHom equals f, i.e., f.toAddHom(x) = f(x) for all x.

Русский

Базовая функция f.toAddHom равна f, то есть для всех x выполняется f.toAddHom(x) = f(x).

LaTeX

$$$\forall x,\; f.toAddHom(x) = f(x)$$$

Lean4

@[simp]
theorem coe_toAddHom (f : M →ₛₗ[σ] M₃) : ⇑f.toAddHom = f :=
  rfl

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

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

Разделы

Аффилиация

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