instAddCommGroup

Mathlib.Topology.Algebra.Module.WeakDual

URI: https://scilib.ai/kg/mathlib#WeakSpace.instAddCommGroup

English

WeakSpace 𝕜 E inherits the structure of an additive commutative group.

Русский

WeakSpace 𝕜 E наследует структуру ADD-коммутативной группы.

LaTeX

$$$AddCommGroup(\\mathrm{WeakSpace } 𝕜 E)$$$

Lean4

instance instAddCommGroup : AddCommGroup (WeakSpace 𝕜 E) :=
  WeakBilin.instAddCommGroup (topDualPairing 𝕜 E).flip

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

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

Разделы

Аффилиация

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