instNonUnitalCommRing — Mathlib

English

If R is a commutative ring and IsTopologicalRing, then the zero-preserving continuous maps C(X, R)₀ form a nonunital commutative ring; operations are defined pointwise and preserve nonunital structure.

Русский

Если R — коммутативное кольцо и IsTopologicalRing, то C(X, R)₀ образуют небазовое (без единицы) коммутативное кольцо; операции определяются по точкам и сохраняют небазовую структуру.

LaTeX

$$$\text{NonUnitalCommRing}(\text{ContinuousMapZero } X\ R)$$$

Lean4

instance instNonUnitalCommRing : NonUnitalCommRing C(X, R)₀ :=
  fast_instance%toContinuousMap_injective.nonUnitalCommRing _ rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ ↦ rfl)
      (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

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