norm_coe — Mathlib

English

The norm on a Submodule s, viewed as a normedAddCommGroup, coincides with the ambient norm via the coercion x ↦ x.

Русский

Норма на подмодуле s, как нормы аддитивной группы, совпадает с нормой в окружении через приведение типов.

LaTeX

$$$ \\| (x : E) \\| = \\|x\\|_s $$$

Lean4

/-- 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

Похожие утверждения