instCommRingOfIsTopologicalRing — Mathlib

English

If β is a commutative ring and IsTopologicalRing holds, then the continuous maps C(α, β) form a commutative ring under pointwise addition and multiplication.

Русский

Если β — коммутативное кольцо и выполняется условие IsTopologicalRing, то непрерывные отображения C(α, β) образуют коммутативное кольцо по точечным операциям сложения и умножения.

LaTeX

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

Lean4

instance {α : Type*} {β : Type*} [TopologicalSpace α] [TopologicalSpace β] [CommRing β] [IsTopologicalRing β] :
    CommRing C(α, β) :=
  coe_injective.commRing _ coe_zero coe_one coe_add coe_mul coe_neg coe_sub coe_nsmul coe_zsmul coe_pow coe_natCast
    coe_intCast

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