instNonUnitalCommRingOfIsTopologicalRing

English

If β is a nonunital commutative ring and α is any space, then the continuous maps C(α, β) inherit a natural structure of a nonunital commutative ring under pointwise addition and multiplication.

Русский

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

LaTeX

$$$ C(\alpha, \beta) \text{ is a nonunital commutative ring with pointwise operations: } (f+g)(x)=f(x)+g(x),\; (f\cdot g)(x)=f(x)g(x). $$$

Lean4

instance {α : Type*} {β : Type*} [TopologicalSpace α] [TopologicalSpace β] [NonUnitalCommRing β] [IsTopologicalRing β] :
    NonUnitalCommRing C(α, β) :=
  coe_injective.nonUnitalCommRing _ coe_zero coe_add coe_mul coe_neg coe_sub coe_nsmul coe_zsmul

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