instVAddSubtypeMem

Mathlib.Algebra.Module.Submodule.Basic

URI: https://scilib.ai/kg/mathlib#Submodule.instVAddSubtypeMem

English

The subtype p inherits a vector addition structure from M, giving a VAdd instance on p.

Русский

Подмножество p наследует структуру векторного сложения от M, образуя VAdd на p.

LaTeX

$$$\text{VAdd } p\;\alpha$ (restrictions of M).$$

Lean4

instance [VAdd M α] : VAdd p α :=
  p.toAddSubmonoid.vadd

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

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

Разделы

Аффилиация

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