instNonAssocRingOfIsTopologicalRing

English

Continuing the above, including negation and subtraction are preserved in C(α, β).

Русский

Продолжая, отрицание и вычитание сохраняются в C(α,β).

LaTeX

$$$\text{instNonUnitalRingOfIsTopologicalRing}(α,β)$$$

Lean4

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

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