Constructing (semi)normed groups from (semi)normed homs

This file defines constructions that upgrade (Comm)Group to (Semi)Normed(Comm)Group using a Group(Semi)normClass when the codomain is the reals.

See Mathlib/Analysis/Normed/Order/Hom/Ultra.lean for further upgrades to nonarchimedean normed groups.

@[reducible, inline]

abbrev GroupSeminormClass.toSeminormedGroup {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [Group α] [GroupSeminormClass F α ℝ] (f : F) : SeminormedGroup α

Constructs a SeminormedGroup structure from a GroupSeminormClass on a Group.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev AddGroupSeminormClass.toSeminormedAddGroup {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [AddGroup α] [AddGroupSeminormClass F α ℝ] (f : F) : SeminormedAddGroup α

Constructs a SeminormedAddGroup structure from an AddGroupSeminormClass on an AddGroup.

Equations

• One or more equations did not get rendered due to their size.

theorem GroupSeminormClass.toSeminormedGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [Group α] [GroupSeminormClass F α ℝ] (f : F) (x : α) : ‖x‖ = f x

theorem AddGroupSeminormClass.toSeminormedAddGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [AddGroup α] [AddGroupSeminormClass F α ℝ] (f : F) (x : α) : ‖x‖ = f x

@[reducible, inline]

abbrev GroupSeminormClass.toSeminormedCommGroup {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [CommGroup α] [GroupSeminormClass F α ℝ] (f : F) : SeminormedCommGroup α

Constructs a SeminormedCommGroup structure from a GroupSeminormClass on a CommGroup.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev AddGroupSeminormClass.toSeminormedAddCommGroup {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [AddCommGroup α] [AddGroupSeminormClass F α ℝ] (f : F) : SeminormedAddCommGroup α

Constructs a SeminormedAddCommGroup structure from an AddGroupSeminormClass on an AddCommGroup.

Equations

• One or more equations did not get rendered due to their size.

theorem GroupSeminormClass.toSeminormedCommGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [CommGroup α] [GroupSeminormClass F α ℝ] (f : F) (x : α) : ‖x‖ = f x

theorem AddGroupSeminormClass.toSeminormedAddCommGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [AddCommGroup α] [AddGroupSeminormClass F α ℝ] (f : F) (x : α) : ‖x‖ = f x

@[reducible, inline]

abbrev GroupNormClass.toNormedGroup {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [Group α] [GroupNormClass F α ℝ] (f : F) : NormedGroup α

Constructs a NormedGroup structure from a GroupNormClass on a Group.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev AddGroupNormClass.toNormedAddGroup {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [AddGroup α] [AddGroupNormClass F α ℝ] (f : F) : NormedAddGroup α

Constructs a NormedAddGroup structure from an AddGroupNormClass on an AddGroup.

Equations

• One or more equations did not get rendered due to their size.

theorem GroupNormClass.toNormedGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [Group α] [GroupNormClass F α ℝ] (f : F) (x : α) : ‖x‖ = f x

theorem AddGroupNormClass.toNormedAddGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [AddGroup α] [AddGroupNormClass F α ℝ] (f : F) (x : α) : ‖x‖ = f x

@[reducible, inline]

abbrev GroupNormClass.toNormedCommGroup {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [CommGroup α] [GroupNormClass F α ℝ] (f : F) : NormedCommGroup α

Constructs a NormedCommGroup structure from a GroupNormClass on a CommGroup.

Equations

• GroupNormClass.toNormedCommGroup f = { toNorm := NormedGroup.toNorm, toGroup := NormedGroup.toGroup, mul_comm := ⋯, toMetricSpace := NormedGroup.toMetricSpace, dist_eq := ⋯ }

@[reducible, inline]

abbrev AddGroupNormClass.toNormedAddCommGroup {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [AddCommGroup α] [AddGroupNormClass F α ℝ] (f : F) : NormedAddCommGroup α

Constructs a NormedAddCommGroup structure from an AddGroupNormClass on an AddCommGroup.

Equations

• One or more equations did not get rendered due to their size.

theorem GroupNormClass.toNormedCommGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [CommGroup α] [GroupNormClass F α ℝ] (f : F) (x : α) : ‖x‖ = f x

theorem AddGroupNormClass.toNormedAddCommGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [AddCommGroup α] [AddGroupNormClass F α ℝ] (f : F) (x : α) : ‖x‖ = f x