instNonUnitalRingOfIsTopologicalRing

English

If β is a (nonunital) ring which is a topological ring, then the compactly supported continuous maps C_c(α, β) form a nonunital ring under pointwise addition and multiplication.

Русский

Если β — кольцо без единицы, но с топологической структурой, то C_c(α, β) компактно поддерживаемых непрерывных отображений образует кольцо без единицы по точечным операциям сложения и умножения.

LaTeX

$$$C_c(\α, β)$ is a NonUnitalRing with pointwise operations.$$

Lean4

instance [NonUnitalRing β] [IsTopologicalRing β] : NonUnitalRing C_c(α, β) :=
  DFunLike.coe_injective.nonUnitalRing _ coe_zero coe_add coe_mul coe_neg coe_sub (fun _ _ => rfl) fun _ _ => rfl

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