Mathlib.Analysis.Normed.Group.Submodule

Submodule.seminormedAddCommGroup instance

[Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] (s : Submodule 𝕜 E) : SeminormedAddCommGroup s

Full source

/-- A submodule of a seminormed group is also a seminormed group, with the restriction of the norm.
-/
instance seminormedAddCommGroup [Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E]
    (s : Submodule 𝕜 E) : SeminormedAddCommGroup s :=
  SeminormedAddCommGroup.induced _ _ s.subtype.toAddMonoidHom

Submodules Inherit Seminormed Additive Commutative Group Structure

Informal description

For any ring $\mathbb{k}$, seminormed additive commutative group $E$ with a $\mathbb{k}$-module structure, and submodule $s$ of $E$, the submodule $s$ inherits a seminormed additive commutative group structure where the norm of an element $x \in s$ is equal to its norm in $E$.

Submodule.coe_norm theorem

[Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {s : Submodule 𝕜 E} (x : s) : ‖x‖ = ‖(x : E)‖

Full source

/-- 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`. -/
@[simp]
theorem coe_norm [Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {s : Submodule 𝕜 E}
    (x : s) : ‖x‖ = ‖(x : E)‖ :=
  rfl

Norm Equality in Submodules: $\|x\|_s = \|x\|_E$

Informal description

Let $\mathbb{k}$ be a ring, $E$ a seminormed additive commutative group with a $\mathbb{k}$-module structure, and $s$ a submodule of $E$. For any element $x \in s$, the norm of $x$ in $s$ is equal to the norm of $x$ when viewed as an element of $E$, i.e., $\|x\|_s = \|x\|_E$.

Submodule.norm_coe theorem

[Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {s : Submodule 𝕜 E} (x : s) : ‖(x : E)‖ = ‖x‖

Full source

/-- 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`. -/
@[norm_cast]
theorem norm_coe [Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {s : Submodule 𝕜 E}
    (x : s) : ‖(x : E)‖ = ‖x‖ :=
  rfl

Norm Equality Between Submodule and Ambient Space

Informal description

Let $\mathbb{k}$ be a ring, $E$ a seminormed additive commutative group with a $\mathbb{k}$-module structure, and $s$ a submodule of $E$. For any element $x \in s$, the norm of $x$ in $E$ is equal to its norm in $s$, i.e., $\|x\|_E = \|x\|_s$.

Submodule.normedAddCommGroup instance

[Ring 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] (s : Submodule 𝕜 E) : NormedAddCommGroup s

Full source

/-- A submodule of a normed group is also a normed group, with the restriction of the norm. -/
instance normedAddCommGroup [Ring 𝕜] [NormedAddCommGroup E] [Module 𝕜 E]
    (s : Submodule 𝕜 E) : NormedAddCommGroup s :=
  { Submodule.seminormedAddCommGroup s with
    eq_of_dist_eq_zero := eq_of_dist_eq_zero }

Submodules Inherit Normed Additive Commutative Group Structure

Informal description

For any ring $\mathbb{k}$, normed additive commutative group $E$ with a $\mathbb{k}$-module structure, and submodule $s$ of $E$, the submodule $s$ inherits a normed additive commutative group structure where the norm of an element $x \in s$ is equal to its norm in $E$.