inftyStarRing

Mathlib.Analysis.Normed.Lp.lpSpace

URI: https://scilib.ai/kg/mathlib#lp.inftyStarRing

Lean4

instance inftyStarRing : StarRing (lp B ∞) :=
  { lp.instStarAddMonoid with star_mul := fun _f _g => ext <| star_mul (R := ∀ i, B i) _ _ }

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

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

Разделы

Аффилиация

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