Documentation

Mathlib.Algebra.Order.Hom.Normed

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.Algebra.Order.Hom.Ultra for further upgrades to nonarchimedean normed groups.

source
@[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
Instances For
    source
    @[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
    Instances For
      source
      theorem AddGroupSeminormClass.toSeminormedAddGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [AddGroup α] [AddGroupSeminormClass F α ℝ] (f : F) (x : α) :
      ‖x‖ = f x
      source
      theorem GroupSeminormClass.toSeminormedGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [Group α] [GroupSeminormClass F α ℝ] (f : F) (x : α) :
      ‖x‖ = f x
      source
      @[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
      Instances For
        source
        @[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
        Instances For
          source
          theorem AddGroupSeminormClass.toSeminormedAddCommGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [AddCommGroup α] [AddGroupSeminormClass F α ℝ] (f : F) (x : α) :
          ‖x‖ = f x
          source
          theorem GroupSeminormClass.toSeminormedCommGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [CommGroup α] [GroupSeminormClass F α ℝ] (f : F) (x : α) :
          ‖x‖ = f x
          source
          @[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
          Instances For
            source
            @[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
            Instances For
              source
              theorem AddGroupNormClass.toNormedAddGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [AddGroup α] [AddGroupNormClass F α ℝ] (f : F) (x : α) :
              ‖x‖ = f x
              source
              theorem GroupNormClass.toNormedGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [Group α] [GroupNormClass F α ℝ] (f : F) (x : α) :
              ‖x‖ = f x
              source
              @[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
              Instances For
                source
                @[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
                Instances For
                  source
                  theorem AddGroupNormClass.toNormedAddCommGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [AddCommGroup α] [AddGroupNormClass F α ℝ] (f : F) (x : α) :
                  ‖x‖ = f x
                  source
                  theorem GroupNormClass.toNormedCommGroup_norm_eq {F : Type u_1} {α : Type u_2} [FunLike F α ℝ] [CommGroup α] [GroupNormClass F α ℝ] (f : F) (x : α) :
                  ‖x‖ = f x