instMulZeroClass

Mathlib.Topology.ContinuousMap.ZeroAtInfty

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

English

C₀(α, β) forms a MulZeroClass under the pointwise operations.

Русский

C₀(α, β) образует MulZeroClass при помощи точечно заданных операций.

LaTeX

$$$ [MulZeroClass \; C_0(\alpha, \beta)] $$$

Lean4

instance instMulZeroClass [MulZeroClass β] [ContinuousMul β] : MulZeroClass C₀(α, β) :=
  DFunLike.coe_injective.mulZeroClass _ coe_zero coe_mul

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

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

Разделы

Аффилиация

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