English
The norm of an element x in a subgroup s, computed in the subgroup, equals the ambient norm: ‖(x:E)‖ = ‖x‖.
Русский
Норма элемента x в подпгуппе s, вычисленная внутри подпгуппы, равна норме в окружении E: ‖(x:E)‖ = ‖x‖.
LaTeX
$$$ ‖(x : E)‖ = ‖x‖ $$$
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`.
This is a reversed version of the `simp` lemma `Subgroup.coe_norm` for use by `norm_cast`. -/
@[to_additive (attr := norm_cast) /-- 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`.
This is a reversed version of the `simp` lemma `AddSubgroup.coe_norm` for use by `norm_cast`. -/
]
theorem norm_coe {s : Subgroup E} (x : s) : ‖(x : E)‖ = ‖x‖ :=
rfl
