coe_norm — Mathlib

English

A submodule of a ring-based seminormed additive group inherits a seminormedAddCommGroup structure via the restricted map.

Русский

Подмодуль кольцевой полугруппы семинормированной группы наследует структуру через ограниченную карту.

LaTeX

$$Instance: Submodule.seminormedAddCommGroup$$

Lean4

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

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