instStarRing

Mathlib.Topology.ContinuousMap.ZeroAtInfty

URI: https://scilib.ai/kg/mathlib#ZeroAtInftyContinuousMap.instStarRing

← MathLib Explorer

English

Under appropriate assumptions, there is a second instance establishing StarRing structure on C0(α,β).

Русский

При надлежащих предположениях существует вторая инстанция StarRing на C0(α,β).

LaTeX

$$StarRing(C0(α,β))$$

Lean4

instance instStarRing : StarRing C₀(α, β) :=
  { ZeroAtInftyContinuousMap.instStarAddMonoid with star_mul := fun f g => ext fun x => star_mul (f x) (g x) }

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

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

Разделы

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

Аффилиация

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