instMulOpposite — Mathlib

English

If the ring is commutative and left-linearly topologized, it is also right-linearly topologized.

Русский

Если кольцо коммутативно и линейно топологизировано слева, то топология линейна и справа.

LaTeX

$$$ [CommRing R] \\Rightarrow IsLinearTopology(R^{op}, R) $$$

Lean4

/-- If `R` is commutative and left-linearly topologized, it is also right-linearly topologized. -/
instance (priority := 100) [IsLinearTopology R R] : IsLinearTopology Rᵐᵒᵖ R := by
  rwa [IsCentralScalar.isLinearTopology_iff]

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