instL1NormedRing

Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.instL1NormedRing

← MathLib Explorer

English

An extended construction provides a full NormedRing structure on tsze R M.

Русский

Расширенная конструкция даёт полную структуру NormedRing на tsze R M.

LaTeX

$$$\\text{NormedRing}(tsze(R,M))$$$

Lean4

instance instL1NormedRing : NormedRing (tsze R M)
    where
  __ : NormedAddCommGroup (tsze R M) := inferInstance
  __ : SeminormedRing (tsze R M) := inferInstance

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

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

Разделы

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

Аффилиация

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