# Subgroups of normed (semi)groups #

In this file, we prove that subgroups of a normed (semi)group are also normed (semi)groups.

## Tags #

normed group

### Subgroups of normed groups #

source
instance Subgroup.seminormedGroup {E : Type u_1} [SeminormedGroup E] {s : Subgroup E} :
SeminormedGroup ↥s

A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.

Equations

- Subgroup.seminormedGroup = SeminormedGroup.induced (↥s) E s.subtype

source
instance AddSubgroup.seminormedAddGroup {E : Type u_1} [SeminormedAddGroup E] {s : AddSubgroup E} :
SeminormedAddGroup ↥s

A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.

Equations

- AddSubgroup.seminormedAddGroup = SeminormedAddGroup.induced (↥s) E s.subtype

source
@[simp]
theorem Subgroup.coe_norm {E : Type u_1} [SeminormedGroup E] {s : Subgroup E} (x : ↥s) :
‖x‖ = ‖↑x‖

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`.

source
@[simp]
theorem AddSubgroup.coe_norm {E : Type u_1} [SeminormedAddGroup E] {s : AddSubgroup E} (x : ↥s) :
‖x‖ = ‖↑x‖

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`.

source
theorem Subgroup.norm_coe {E : Type u_1} [SeminormedGroup E] {s : Subgroup E} (x : ↥s) :
‖↑x‖ = ‖x‖

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`.

source
theorem AddSubgroup.norm_coe {E : Type u_1} [SeminormedAddGroup E] {s : AddSubgroup E} (x : ↥s) :
‖↑x‖ = ‖x‖

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`.

source
instance Subgroup.seminormedCommGroup {E : Type u_1} [SeminormedCommGroup E] {s : Subgroup E} :
SeminormedCommGroup ↥s
Equations

- Subgroup.seminormedCommGroup = SeminormedCommGroup.induced (↥s) E s.subtype

source
instance AddSubgroup.seminormedAddCommGroup {E : Type u_1} [SeminormedAddCommGroup E] {s : AddSubgroup E} :
SeminormedAddCommGroup ↥s
Equations

- AddSubgroup.seminormedAddCommGroup = SeminormedAddCommGroup.induced (↥s) E s.subtype

source
instance Subgroup.normedGroup {E : Type u_1} [NormedGroup E] {s : Subgroup E} :
NormedGroup ↥s
Equations

- Subgroup.normedGroup = NormedGroup.induced (↥s) E s.subtype ⋯

source
instance AddSubgroup.normedAddGroup {E : Type u_1} [NormedAddGroup E] {s : AddSubgroup E} :
NormedAddGroup ↥s
Equations

- AddSubgroup.normedAddGroup = NormedAddGroup.induced (↥s) E s.subtype ⋯

source
instance Subgroup.normedCommGroup {E : Type u_1} [NormedCommGroup E] {s : Subgroup E} :
NormedCommGroup ↥s
Equations

- Subgroup.normedCommGroup = NormedCommGroup.induced (↥s) E s.subtype ⋯

source
instance AddSubgroup.normedAddCommGroup {E : Type u_1} [NormedAddCommGroup E] {s : AddSubgroup E} :
NormedAddCommGroup ↥s
Equations

- AddSubgroup.normedAddCommGroup = NormedAddCommGroup.induced (↥s) E s.subtype ⋯

### Subgroup classes of normed groups #

source
@[instance 75]
instance SubgroupClass.seminormedGroup {E : Type u_1} [SeminormedGroup E] {S : Type u_2} [SetLike S E] [SubgroupClass S E] (s : S) :
SeminormedGroup ↥s

A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.

Equations

- SubgroupClass.seminormedGroup s = SeminormedGroup.induced (↥s) E ↑s

source
@[instance 75]
instance AddSubgroupClass.seminormedAddGroup {E : Type u_1} [SeminormedAddGroup E] {S : Type u_2} [SetLike S E] [AddSubgroupClass S E] (s : S) :
SeminormedAddGroup ↥s

A subgroup of a seminormed additive group is also a seminormed additive group, with the restriction of the norm.

Equations

- AddSubgroupClass.seminormedAddGroup s = SeminormedAddGroup.induced (↥s) E ↑s

source
@[simp]
theorem SubgroupClass.coe_norm {E : Type u_1} [SeminormedGroup E] {S : Type u_2} [SetLike S E] [SubgroupClass S E] (s : S) (x : ↥s) :
‖x‖ = ‖↑x‖

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`.

source
@[simp]
theorem AddSubgroupClass.coe_norm {E : Type u_1} [SeminormedAddGroup E] {S : Type u_2} [SetLike S E] [AddSubgroupClass S E] (s : S) (x : ↥s) :
‖x‖ = ‖↑x‖

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`.

source
@[instance 75]
instance SubgroupClass.seminormedCommGroup {E : Type u_1} [SeminormedCommGroup E] {S : Type u_2} [SetLike S E] [SubgroupClass S E] (s : S) :
SeminormedCommGroup ↥s
Equations

- SubgroupClass.seminormedCommGroup s = SeminormedCommGroup.induced (↥s) E ↑s

source
@[instance 75]
instance AddSubgroupClass.seminormedAddCommGroup {E : Type u_1} [SeminormedAddCommGroup E] {S : Type u_2} [SetLike S E] [AddSubgroupClass S E] (s : S) :
SeminormedAddCommGroup ↥s
Equations

- AddSubgroupClass.seminormedAddCommGroup s = SeminormedAddCommGroup.induced (↥s) E ↑s

source
@[instance 75]
instance SubgroupClass.normedGroup {E : Type u_1} [NormedGroup E] {S : Type u_2} [SetLike S E] [SubgroupClass S E] (s : S) :
NormedGroup ↥s
Equations

- SubgroupClass.normedGroup s = NormedGroup.induced (↥s) E ↑s ⋯

source
@[instance 75]
instance AddSubgroupClass.normedAddGroup {E : Type u_1} [NormedAddGroup E] {S : Type u_2} [SetLike S E] [AddSubgroupClass S E] (s : S) :
NormedAddGroup ↥s
Equations

- AddSubgroupClass.normedAddGroup s = NormedAddGroup.induced (↥s) E ↑s ⋯

source
@[instance 75]
instance SubgroupClass.normedCommGroup {E : Type u_1} [NormedCommGroup E] {S : Type u_2} [SetLike S E] [SubgroupClass S E] (s : S) :
NormedCommGroup ↥s
Equations

- SubgroupClass.normedCommGroup s = NormedCommGroup.induced (↥s) E ↑s ⋯

source
@[instance 75]
instance AddSubgroupClass.normedAddCommGroup {E : Type u_1} [NormedAddCommGroup E] {S : Type u_2} [SetLike S E] [AddSubgroupClass S E] (s : S) :
NormedAddCommGroup ↥s
Equations

- AddSubgroupClass.normedAddCommGroup s = NormedAddCommGroup.induced (↥s) E ↑s ⋯