instIsTopologicalRingMulOpposite

Mathlib.Topology.Algebra.Ring.Basic

URI: https://scilib.ai/kg/mathlib#instIsTopologicalRingMulOpposite

English

If R is a nonunital nonassociative ring and IsTopologicalRing R, then IsTopologicalRing (MulOpposite R).

Русский

Если R — безединичное неассоциативное кольцо и IsTopologicalRing R, то IsTopologicalRing(MulOpposite R).

LaTeX

$$IsTopologicalRing (MulOpposite R)$$

Lean4

instance [NonUnitalNonAssocRing R] [TopologicalSpace R] [IsTopologicalRing R] : IsTopologicalRing Rᵐᵒᵖ :=
  ⟨⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru