coe_norm — Mathlib

English

For x ∈ s, the subgroup norm equals ambient norm: ‖x‖ = ‖(x:E)‖.

Русский

Для x ∈ s норма подпгуппы равна норме в E: ‖x‖ = ‖(x:E)‖.

LaTeX

$$$ ‖x‖ = ‖(x : E)‖ $$$

Lean4

/-- If `x` is an element of a subgroup `s` of a seminormed group `E`, its norm in `s` is equal to
its norm in `E`. -/
@[to_additive (attr := simp) /-- If `x` is an element of an additive subgroup `s` of a seminormed
    additive group `E`, its norm in `s` is equal to its norm in `E`. -/
    ]
theorem coe_norm (x : s) : ‖x‖ = ‖(x : E)‖ :=
  rfl

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