continuousSMul — Mathlib

English

Under IsTopologicalRing R, the ModuleFilterBasis gives a continuous scalar action on M; i.e., the map (r,m) ↦ r · m is continuous.

Русский

При условии IsTopologicalRing R модульная фильтр-база задаёт непрерывное скалярное действие на M.

LaTeX

$$$\text{ContinuousSMul}(R,M)$.$$

Lean4

/-- If a module is endowed with a topological structure coming from
a module filter basis then it's a topological module. -/
instance (priority := 100) continuousSMul [IsTopologicalRing R] : @ContinuousSMul R M _ _ B.topology :=
  by
  let B' := B.toAddGroupFilterBasis
  let _ := B'.topology
  have _ := B'.isTopologicalAddGroup
  exact
    ContinuousSMul.of_basis_zero B'.nhds_zero_hasBasis (fun {_} => by simpa using B.smul) (by simpa using B.smul_left)
      B.smul_right

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