Submodules of normed groups

instance Submodule.seminormedAddCommGroup {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] (s : Submodule 𝕜 E) : SeminormedAddCommGroup ↥s

A submodule of a seminormed group is also a seminormed group, with the restriction of the norm.

Equations

• s.seminormedAddCommGroup = SeminormedAddCommGroup.induced (↥s) E s.subtype.toAddMonoidHom

@[simp]

theorem Submodule.coe_norm {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {s : Submodule 𝕜 E} (x : ↥s) : ‖x‖ = ‖↑x‖

If x is an element of a submodule s of a normed group E, its norm in s is equal to its norm in E.

theorem Submodule.norm_coe {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {s : Submodule 𝕜 E} (x : ↥s) : ‖↑x‖ = ‖x‖

If x is an element of a submodule s of a normed group E, its norm in E is equal to its norm in s.

This is a reversed version of the simp lemma Submodule.coe_norm for use by norm_cast.

instance Submodule.normedAddCommGroup {𝕜 : Type u_1} {E : Type u_2} [Ring 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] (s : Submodule 𝕜 E) : NormedAddCommGroup ↥s

A submodule of a normed group is also a normed group, with the restriction of the norm.

Equations

• s.normedAddCommGroup = let __src := s.seminormedAddCommGroup; NormedAddCommGroup.mk ⋯