Dual

Mathlib.LinearAlgebra.Dual.Defs

URI: https://scilib.ai/kg/mathlib#Module.Dual

English

The dual space of an R-module M is the module of linear maps M → R over R.

Русский

Двойственное пространство модуля M над кольцом R есть модуль линейных отображений M → R над R.

LaTeX

$$$ \\mathrm{Dual} := M \\to_\\text{linear} R $$$

Lean4

/-- The dual space of an R-module M is the R-module of linear maps `M → R`. -/
abbrev Dual :=
  M →ₗ[R] R

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

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

Разделы

Аффилиация

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