normedAddCommGroup

Mathlib.Analysis.Normed.Group.Quotient

URI: https://scilib.ai/kg/mathlib#Submodule.Quotient.normedAddCommGroup

← MathLib Explorer

English

The quotient inherits a bounded scalar multiplication from a suitable scalar ring 𝕜.

Русский

Квадрирование скалярного умножения переходит на факторное пространство M/S.

LaTeX

$$Submodule.Quotient.instIsBoundedSMul$$

Lean4

instance normedAddCommGroup [hS : IsClosed (S : Set M)] : NormedAddCommGroup (M ⧸ S) :=
  QuotientAddGroup.instNormedAddCommGroup S.toAddSubgroup (hS := hS)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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