instNonUnitalRing — Mathlib

English

C₀(α,β) forms a NonUnitalRing when β is a NonUnitalRing and IsTopologicalRing.

Русский

C₀(α,β) образует NonUnitalRing, если β — NonUnitalRing и IsTopologicalRing.

LaTeX

$$NonUnitalRing C₀(α, β) with (f−g) and (f·g) defined pointwise.$$

Lean4

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

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