Bounded scalar actions on submodules of seminormed modules

Mathlib equips submodules and closed submodules of a seminormed module over a ring with the restricted seminorm (Submodule.seminormedAddCommGroup, ClosedSubmodule.seminormedAddCommGroup), and equips them with NormedSpace when the scalar ring is a normed field (Submodule.normedSpace, ClosedSubmodule.normedSpace). When the scalars form a general seminormed ring acting with IsBoundedSMul, the restricted action on any submodule or closed submodule is again contractive (IsBoundedSMul), because the norm of a subtype element equals its ambient norm.

instance Submodule.instIsBoundedSMul {R : Type u_1} {M : Type u_2} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] (S : Submodule R M) : IsBoundedSMul R ↥S

A submodule of a seminormed module with a bounded scalar action inherits a bounded scalar action under the subspace norm.

instance ClosedSubmodule.instIsBoundedSMul {R : Type u_1} {M : Type u_2} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] (S : ClosedSubmodule R M) : IsBoundedSMul R ↥S

A closed submodule of a seminormed module with a bounded scalar action inherits a bounded scalar action under the subspace norm.