Submodules of normed groups

@[instance_reducible]

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 = { norm := fun (a : ↥s) => ‖s.subtype.toAddMonoidHom a‖, toAddCommGroup := s.addCommGroup, toPseudoMetricSpace := Subtype.pseudoMetricSpace, dist_eq := ⋯ }

@[deprecated "use `norm_coe`" (since := "2026-08-25")]

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.

@[instance_reducible]

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

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

@[instance_reducible]

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

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

Equations

• s.normedAddCommGroup = { toNorm := s.seminormedAddCommGroup.toNorm, toAddCommGroup := s.seminormedAddCommGroup.toAddCommGroup, toMetricSpace := Subtype.metricSpace, dist_eq := ⋯ }

theorem LinearMap.continuous_domRestrict {R : Type u_3} {R' : Type u_4} {M : Type u_5} {M' : Type u_6} [Semiring R] [Semiring R'] [AddCommMonoid M] [AddCommMonoid M'] [Module R M] [Module R' M'] {σ₁₂ : R →+* R'} (f : M →ₛₗ[σ₁₂] M') [TopologicalSpace M] [TopologicalSpace M'] (hf : Continuous ⇑f) (p : Submodule R M) : Continuous ⇑(f.domRestrict p)