toOppositeIsModuleTopology — Mathlib

English

The module topology coming from the action of the opposite ring Rᵐᵒᵖ on R is the same as R's topology.

Русский

Модульная топология, полученная от действия противоположного кольца Rᵐᵒᵖ на R, совпадает с топологией R.

LaTeX

$$$\text{IsModuleTopology } R^{\mathrm{mop}} R$ is given by the iso $\text{MulOpposite.opContinuousLinearEquiv } R^{\mathrm{mop}}$$$

Lean4

/-- The module topology coming from the action of the topological ring `Rᵐᵒᵖ` on `R`
  (via `Semiring.toOppositeModule`, i.e. via `(op r) • m = m * r`) is `R`'s topology. -/
instance _root_.IsTopologicalSemiring.toOppositeIsModuleTopology : IsModuleTopology Rᵐᵒᵖ R :=
  .iso (MulOpposite.opContinuousLinearEquiv Rᵐᵒᵖ).symm

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