\import Algebra.Module
\import Algebra.Monoid
\import Algebra.Ring
\import Arith.Real
\import Paths
\import Topology.NormedAbGroup
\import Topology.NormedRing

\class PseudoNormedLModule \extends LModule, PseudoNormedAbGroup {
  \override R : PseudoNormedRing
  | norm_*c {a : R} {x : E} : norm (a *c x) = norm {R} a * norm x
}

\class NormedLModule \extends PseudoNormedLModule, NormedAbGroup

\class CompleteNormedLModule \extends NormedLModule, CompleteNormedAbGroup

\lemma norm_ide=0-module {R : PseudoNormedRing} {X : PseudoNormedLModule R} (p : R.norm  = ( : Real)) {x : X} : norm x = ( : Real)
  => pmap norm (inv ide_*c) *> norm_*c *> pmap (`* _) p *> Ring.zro_*-left