instIsLinearTopologyOfMulOpposite

English

If R has a linear topology, then the space of multivariate power series MvPowerSeries(σ,R), with the product topology, carries a left linear topology (i.e., a linear-topology structure compatible with left scalar action).

Русский

Если R обладает линейной топологией, то пространство многомерных степенных рядов MvPowerSeries(σ,R) с произведенной топологией обладает слева линейной топологией (структура линейной топологии совместима с действием слева по R).

LaTeX

$$$\operatorname{IsLinearTopology}\bigl(\mathrm{MvPowerSeries}(\sigma,R),\ \mathrm{MvPowerSeries}(\sigma,R)\bigr).$$$

Lean4

/-- The topology on `MvPowerSeries` is a left linear topology
  when the ring of coefficients has a linear topology. -/
instance [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] : IsLinearTopology (MvPowerSeries σ R) (MvPowerSeries σ R) :=
  IsLinearTopology.mk_of_hasBasis' _ hasBasis_nhds_zero TwoSidedIdeal.mul_mem_left

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