Documentation

Mathlib.Analysis.Normed.Field.Basic

Normed fields #

In this file we define (semi)normed rings and fields. We also prove some theorems about these definitions.

A non-unital seminormed ring is a not-necessarily-unital ring endowed with a seminorm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

Instances
    theorem NonUnitalSeminormedRing.dist_eq {α : Type u_5} [self : NonUnitalSeminormedRing α] (x : α) (y : α) :
    dist x y = x - y

    The distance is induced by the norm.

    theorem NonUnitalSeminormedRing.norm_mul {α : Type u_5} [self : NonUnitalSeminormedRing α] (a : α) (b : α) :

    The norm is submultiplicative.

    class SeminormedRing (α : Type u_5) extends Norm , Ring , PseudoMetricSpace :
    Type u_5

    A seminormed ring is a ring endowed with a seminorm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

    Instances
      theorem SeminormedRing.dist_eq {α : Type u_5} [self : SeminormedRing α] (x : α) (y : α) :
      dist x y = x - y

      The distance is induced by the norm.

      theorem SeminormedRing.norm_mul {α : Type u_5} [self : SeminormedRing α] (a : α) (b : α) :

      The norm is submultiplicative.

      @[instance 100]

      A seminormed ring is a non-unital seminormed ring.

      Equations
      class NonUnitalNormedRing (α : Type u_5) extends Norm , NonUnitalRing , MetricSpace :
      Type u_5

      A non-unital normed ring is a not-necessarily-unital ring endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

      Instances
        theorem NonUnitalNormedRing.dist_eq {α : Type u_5} [self : NonUnitalNormedRing α] (x : α) (y : α) :
        dist x y = x - y

        The distance is induced by the norm.

        theorem NonUnitalNormedRing.norm_mul {α : Type u_5} [self : NonUnitalNormedRing α] (a : α) (b : α) :

        The norm is submultiplicative.

        @[instance 100]

        A non-unital normed ring is a non-unital seminormed ring.

        Equations
        class NormedRing (α : Type u_5) extends Norm , Ring , MetricSpace :
        Type u_5

        A normed ring is a ring endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

        Instances
          theorem NormedRing.dist_eq {α : Type u_5} [self : NormedRing α] (x : α) (y : α) :
          dist x y = x - y

          The distance is induced by the norm.

          theorem NormedRing.norm_mul {α : Type u_5} [self : NormedRing α] (a : α) (b : α) :

          The norm is submultiplicative.

          class NormedDivisionRing (α : Type u_5) extends Norm , DivisionRing , MetricSpace :
          Type u_5

          A normed division ring is a division ring endowed with a seminorm which satisfies the equality ‖x y‖ = ‖x‖ ‖y‖.

          Instances
            theorem NormedDivisionRing.dist_eq {α : Type u_5} [self : NormedDivisionRing α] (x : α) (y : α) :
            dist x y = x - y

            The distance is induced by the norm.

            theorem NormedDivisionRing.norm_mul' {α : Type u_5} [self : NormedDivisionRing α] (a : α) (b : α) :

            The norm is multiplicative.

            @[instance 100]

            A normed division ring is a normed ring.

            Equations
            @[instance 100]
            instance NormedRing.toSeminormedRing {α : Type u_1} [β : NormedRing α] :

            A normed ring is a seminormed ring.

            Equations
            @[instance 100]

            A normed ring is a non-unital normed ring.

            Equations

            A non-unital seminormed commutative ring is a non-unital commutative ring endowed with a seminorm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

            Instances
              theorem NonUnitalSeminormedCommRing.mul_comm {α : Type u_5} [self : NonUnitalSeminormedCommRing α] (x : α) (y : α) :
              x * y = y * x

              Multiplication is commutative.

              A non-unital normed commutative ring is a non-unital commutative ring endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

              Instances
                theorem NonUnitalNormedCommRing.mul_comm {α : Type u_5} [self : NonUnitalNormedCommRing α] (x : α) (y : α) :
                x * y = y * x

                Multiplication is commutative.

                @[instance 100]

                A non-unital normed commutative ring is a non-unital seminormed commutative ring.

                Equations
                class SeminormedCommRing (α : Type u_5) extends SeminormedRing :
                Type u_5

                A seminormed commutative ring is a commutative ring endowed with a seminorm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

                Instances
                  theorem SeminormedCommRing.mul_comm {α : Type u_5} [self : SeminormedCommRing α] (x : α) (y : α) :
                  x * y = y * x

                  Multiplication is commutative.

                  class NormedCommRing (α : Type u_5) extends NormedRing :
                  Type u_5

                  A normed commutative ring is a commutative ring endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖.

                  Instances
                    theorem NormedCommRing.mul_comm {α : Type u_5} [self : NormedCommRing α] (x : α) (y : α) :
                    x * y = y * x

                    Multiplication is commutative.

                    @[instance 100]

                    A seminormed commutative ring is a non-unital seminormed commutative ring.

                    Equations
                    @[instance 100]

                    A normed commutative ring is a non-unital normed commutative ring.

                    Equations
                    @[instance 100]

                    A normed commutative ring is a seminormed commutative ring.

                    Equations
                    class NormOneClass (α : Type u_5) [Norm α] [One α] :

                    A mixin class with the axiom ‖1‖ = 1. Many NormedRings and all NormedFields satisfy this axiom.

                    • norm_one : 1 = 1

                      The norm of the multiplicative identity is 1.

                    Instances
                      @[simp]
                      theorem NormOneClass.norm_one {α : Type u_5} [Norm α] [One α] [self : NormOneClass α] :

                      The norm of the multiplicative identity is 1.

                      @[simp]
                      theorem nnnorm_one {α : Type u_1} [SeminormedAddCommGroup α] [One α] [NormOneClass α] :
                      @[instance 100]
                      Equations
                      @[instance 100]
                      Equations
                      @[instance 100]
                      Equations
                      @[instance 100]
                      Equations
                      Equations
                      • =
                      instance Prod.normOneClass {α : Type u_1} {β : Type u_2} [SeminormedAddCommGroup α] [One α] [NormOneClass α] [SeminormedAddCommGroup β] [One β] [NormOneClass β] :
                      Equations
                      • =
                      instance Pi.normOneClass {ι : Type u_5} {α : ιType u_6} [Nonempty ι] [Fintype ι] [(i : ι) → SeminormedAddCommGroup (α i)] [(i : ι) → One (α i)] [∀ (i : ι), NormOneClass (α i)] :
                      NormOneClass ((i : ι) → α i)
                      Equations
                      • =
                      theorem norm_mul_le {α : Type u_1} [NonUnitalSeminormedRing α] (a : α) (b : α) :
                      theorem nnnorm_mul_le {α : Type u_1} [NonUnitalSeminormedRing α] (a : α) (b : α) :
                      theorem one_le_norm_one (β : Type u_5) [NormedRing β] [Nontrivial β] :
                      theorem Filter.Tendsto.zero_mul_isBoundedUnder_le {α : Type u_1} {ι : Type u_4} [NonUnitalSeminormedRing α] {f : ια} {g : ια} {l : Filter ι} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l ((fun (x : α) => x) g)) :
                      Filter.Tendsto (fun (x : ι) => f x * g x) l (nhds 0)
                      theorem Filter.isBoundedUnder_le_mul_tendsto_zero {α : Type u_1} {ι : Type u_4} [NonUnitalSeminormedRing α] {f : ια} {g : ια} {l : Filter ι} (hf : Filter.IsBoundedUnder (fun (x x_1 : ) => x x_1) l (norm f)) (hg : Filter.Tendsto g l (nhds 0)) :
                      Filter.Tendsto (fun (x : ι) => f x * g x) l (nhds 0)
                      theorem mulLeft_bound {α : Type u_1} [NonUnitalSeminormedRing α] (x : α) (y : α) :

                      In a seminormed ring, the left-multiplication AddMonoidHom is bounded.

                      theorem mulRight_bound {α : Type u_1} [NonUnitalSeminormedRing α] (x : α) (y : α) :

                      In a seminormed ring, the right-multiplication AddMonoidHom is bounded.

                      A non-unital subalgebra of a non-unital seminormed ring is also a non-unital seminormed ring, with the restriction of the norm.

                      Equations
                      • s.nonUnitalSeminormedRing = let __src := s.toSubmodule.seminormedAddCommGroup; let __src_1 := s.toNonUnitalRing; NonUnitalSeminormedRing.mk

                      A non-unital subalgebra of a non-unital normed ring is also a non-unital normed ring, with the restriction of the norm.

                      Equations
                      Equations
                      • ULift.nonUnitalSeminormedRing = let __src := ULift.seminormedAddCommGroup; let __src_1 := ULift.nonUnitalRing; NonUnitalSeminormedRing.mk

                      Non-unital seminormed ring structure on the product of two non-unital seminormed rings, using the sup norm.

                      Equations
                      • Prod.nonUnitalSeminormedRing = let __src := Prod.seminormedAddCommGroup; let __src_1 := Prod.instNonUnitalRing; NonUnitalSeminormedRing.mk
                      instance Pi.nonUnitalSeminormedRing {ι : Type u_4} {π : ιType u_5} [Fintype ι] [(i : ι) → NonUnitalSeminormedRing (π i)] :
                      NonUnitalSeminormedRing ((i : ι) → π i)

                      Non-unital seminormed ring structure on the product of finitely many non-unital seminormed rings, using the sup norm.

                      Equations
                      • Pi.nonUnitalSeminormedRing = let __src := Pi.seminormedAddCommGroup; let __src_1 := Pi.nonUnitalRing; NonUnitalSeminormedRing.mk
                      Equations
                      • MulOpposite.instNonUnitalSeminormedRing = let __spread.0 := MulOpposite.instNonUnitalRing; let __spread.1 := MulOpposite.instSeminormedAddCommGroup; NonUnitalSeminormedRing.mk
                      instance Subalgebra.seminormedRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [SeminormedRing E] [Algebra 𝕜 E] (s : Subalgebra 𝕜 E) :

                      A subalgebra of a seminormed ring is also a seminormed ring, with the restriction of the norm.

                      Equations
                      • s.seminormedRing = let __src := (Subalgebra.toSubmodule s).seminormedAddCommGroup; let __src_1 := s.toRing; SeminormedRing.mk
                      instance Subalgebra.normedRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [NormedRing E] [Algebra 𝕜 E] (s : Subalgebra 𝕜 E) :

                      A subalgebra of a normed ring is also a normed ring, with the restriction of the norm.

                      Equations
                      theorem Nat.norm_cast_le {α : Type u_1} [SeminormedRing α] (n : ) :
                      n n * 1
                      theorem List.norm_prod_le' {α : Type u_1} [SeminormedRing α] {l : List α} :
                      l []l.prod (List.map norm l).prod
                      theorem List.nnnorm_prod_le' {α : Type u_1} [SeminormedRing α] {l : List α} (hl : l []) :
                      l.prod‖₊ (List.map nnnorm l).prod
                      theorem List.norm_prod_le {α : Type u_1} [SeminormedRing α] [NormOneClass α] (l : List α) :
                      l.prod (List.map norm l).prod
                      theorem List.nnnorm_prod_le {α : Type u_1} [SeminormedRing α] [NormOneClass α] (l : List α) :
                      l.prod‖₊ (List.map nnnorm l).prod
                      theorem Finset.norm_prod_le' {ι : Type u_4} {α : Type u_5} [NormedCommRing α] (s : Finset ι) (hs : s.Nonempty) (f : ια) :
                      is, f i is, f i
                      theorem Finset.nnnorm_prod_le' {ι : Type u_4} {α : Type u_5} [NormedCommRing α] (s : Finset ι) (hs : s.Nonempty) (f : ια) :
                      is, f i‖₊ is, f i‖₊
                      theorem Finset.norm_prod_le {ι : Type u_4} {α : Type u_5} [NormedCommRing α] [NormOneClass α] (s : Finset ι) (f : ια) :
                      is, f i is, f i
                      theorem Finset.nnnorm_prod_le {ι : Type u_4} {α : Type u_5} [NormedCommRing α] [NormOneClass α] (s : Finset ι) (f : ια) :
                      is, f i‖₊ is, f i‖₊
                      theorem nnnorm_pow_le' {α : Type u_1} [SeminormedRing α] (a : α) {n : } :
                      0 < na ^ n‖₊ a‖₊ ^ n

                      If α is a seminormed ring, then ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n for n > 0. See also nnnorm_pow_le.

                      theorem nnnorm_pow_le {α : Type u_1} [SeminormedRing α] [NormOneClass α] (a : α) (n : ) :

                      If α is a seminormed ring with ‖1‖₊ = 1, then ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n. See also nnnorm_pow_le'.

                      theorem norm_pow_le' {α : Type u_1} [SeminormedRing α] (a : α) {n : } (h : 0 < n) :

                      If α is a seminormed ring, then ‖a ^ n‖ ≤ ‖a‖ ^ n for n > 0. See also norm_pow_le.

                      theorem norm_pow_le {α : Type u_1} [SeminormedRing α] [NormOneClass α] (a : α) (n : ) :

                      If α is a seminormed ring with ‖1‖ = 1, then ‖a ^ n‖ ≤ ‖a‖ ^ n. See also norm_pow_le'.

                      theorem eventually_norm_pow_le {α : Type u_1} [SeminormedRing α] (a : α) :
                      ∀ᶠ (n : ) in Filter.atTop, a ^ n a ^ n
                      Equations
                      • ULift.seminormedRing = let __src := ULift.nonUnitalSeminormedRing; let __src_1 := ULift.ring; SeminormedRing.mk
                      instance Prod.seminormedRing {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedRing β] :

                      Seminormed ring structure on the product of two seminormed rings, using the sup norm.

                      Equations
                      • Prod.seminormedRing = let __src := Prod.nonUnitalSeminormedRing; let __src_1 := Prod.instRing; SeminormedRing.mk
                      instance Pi.seminormedRing {ι : Type u_4} {π : ιType u_5} [Fintype ι] [(i : ι) → SeminormedRing (π i)] :
                      SeminormedRing ((i : ι) → π i)

                      Seminormed ring structure on the product of finitely many seminormed rings, using the sup norm.

                      Equations
                      • Pi.seminormedRing = let __src := Pi.nonUnitalSeminormedRing; let __src_1 := Pi.ring; SeminormedRing.mk
                      Equations
                      • MulOpposite.instSeminormedRing = let __spread.0 := MulOpposite.instRing; let __spread.1 := MulOpposite.instNonUnitalSeminormedRing; SeminormedRing.mk
                      Equations
                      • ULift.nonUnitalNormedRing = let __src := ULift.nonUnitalSeminormedRing; let __src_1 := ULift.normedAddCommGroup; NonUnitalNormedRing.mk

                      Non-unital normed ring structure on the product of two non-unital normed rings, using the sup norm.

                      Equations
                      • Prod.nonUnitalNormedRing = let __src := Prod.nonUnitalSeminormedRing; let __src_1 := Prod.normedAddCommGroup; NonUnitalNormedRing.mk
                      instance Pi.nonUnitalNormedRing {ι : Type u_4} {π : ιType u_5} [Fintype ι] [(i : ι) → NonUnitalNormedRing (π i)] :
                      NonUnitalNormedRing ((i : ι) → π i)

                      Normed ring structure on the product of finitely many non-unital normed rings, using the sup norm.

                      Equations
                      • Pi.nonUnitalNormedRing = let __src := Pi.nonUnitalSeminormedRing; let __src_1 := Pi.normedAddCommGroup; NonUnitalNormedRing.mk
                      Equations
                      • One or more equations did not get rendered due to their size.
                      theorem Units.norm_pos {α : Type u_1} [NormedRing α] [Nontrivial α] (x : αˣ) :
                      0 < x
                      theorem Units.nnnorm_pos {α : Type u_1} [NormedRing α] [Nontrivial α] (x : αˣ) :
                      0 < x‖₊
                      Equations
                      • ULift.normedRing = let __src := ULift.seminormedRing; let __src_1 := ULift.normedAddCommGroup; NormedRing.mk
                      instance Prod.normedRing {α : Type u_1} {β : Type u_2} [NormedRing α] [NormedRing β] :
                      NormedRing (α × β)

                      Normed ring structure on the product of two normed rings, using the sup norm.

                      Equations
                      • Prod.normedRing = let __src := Prod.nonUnitalNormedRing; let __src_1 := Prod.instRing; NormedRing.mk
                      instance Pi.normedRing {ι : Type u_4} {π : ιType u_5} [Fintype ι] [(i : ι) → NormedRing (π i)] :
                      NormedRing ((i : ι) → π i)

                      Normed ring structure on the product of finitely many normed rings, using the sup norm.

                      Equations
                      • Pi.normedRing = let __src := Pi.seminormedRing; let __src_1 := Pi.normedAddCommGroup; NormedRing.mk
                      Equations
                      • MulOpposite.instNormedRing = let __spread.0 := MulOpposite.instRing; let __spread.1 := MulOpposite.instSeminormedRing; let __spread.2 := MulOpposite.instNormedAddCommGroup; NormedRing.mk
                      Equations

                      Non-unital seminormed commutative ring structure on the product of two non-unital seminormed commutative rings, using the sup norm.

                      Equations
                      • Prod.nonUnitalSeminormedCommRing = let __src := Prod.nonUnitalSeminormedRing; let __src_1 := Prod.instNonUnitalCommRing; NonUnitalSeminormedCommRing.mk
                      instance Pi.nonUnitalSeminormedCommRing {ι : Type u_4} {π : ιType u_5} [Fintype ι] [(i : ι) → NonUnitalSeminormedCommRing (π i)] :
                      NonUnitalSeminormedCommRing ((i : ι) → π i)

                      Non-unital seminormed commutative ring structure on the product of finitely many non-unital seminormed commutative rings, using the sup norm.

                      Equations
                      Equations
                      • MulOpposite.instNonUnitalSeminormedCommRing = let __spread.0 := MulOpposite.instNonUnitalSeminormedRing; let __spread.1 := MulOpposite.instNonUnitalCommRing; NonUnitalSeminormedCommRing.mk

                      A non-unital subalgebra of a non-unital seminormed commutative ring is also a non-unital seminormed commutative ring, with the restriction of the norm.

                      Equations

                      A non-unital subalgebra of a non-unital normed commutative ring is also a non-unital normed commutative ring, with the restriction of the norm.

                      Equations
                      • s.nonUnitalNormedCommRing = let __src := s.nonUnitalSeminormedCommRing; let __src_1 := s.nonUnitalNormedRing; NonUnitalNormedCommRing.mk
                      Equations
                      • ULift.nonUnitalNormedCommRing = let __src := ULift.nonUnitalSeminormedCommRing; let __src_1 := ULift.normedAddCommGroup; NonUnitalNormedCommRing.mk

                      Non-unital normed commutative ring structure on the product of two non-unital normed commutative rings, using the sup norm.

                      Equations
                      • Prod.nonUnitalNormedCommRing = let __src := Prod.nonUnitalSeminormedCommRing; let __src_1 := Prod.normedAddCommGroup; NonUnitalNormedCommRing.mk
                      instance Pi.nonUnitalNormedCommRing {ι : Type u_4} {π : ιType u_5} [Fintype ι] [(i : ι) → NonUnitalNormedCommRing (π i)] :
                      NonUnitalNormedCommRing ((i : ι) → π i)

                      Normed commutative ring structure on the product of finitely many non-unital normed commutative rings, using the sup norm.

                      Equations
                      • Pi.nonUnitalNormedCommRing = let __src := Pi.nonUnitalSeminormedCommRing; let __src_1 := Pi.normedAddCommGroup; NonUnitalNormedCommRing.mk
                      Equations
                      • MulOpposite.instNonUnitalNormedCommRing = let __spread.0 := MulOpposite.instNonUnitalNormedRing; let __spread.1 := MulOpposite.instNonUnitalSeminormedCommRing; NonUnitalNormedCommRing.mk
                      Equations
                      • ULift.seminormedCommRing = let __src := ULift.nonUnitalSeminormedRing; let __src_1 := ULift.commRing; SeminormedCommRing.mk

                      Seminormed commutative ring structure on the product of two seminormed commutative rings, using the sup norm.

                      Equations
                      • Prod.seminormedCommRing = let __src := Prod.nonUnitalSeminormedCommRing; let __src_1 := Prod.instCommRing; SeminormedCommRing.mk
                      instance Pi.seminormedCommRing {ι : Type u_4} {π : ιType u_5} [Fintype ι] [(i : ι) → SeminormedCommRing (π i)] :
                      SeminormedCommRing ((i : ι) → π i)

                      Seminormed commutative ring structure on the product of finitely many seminormed commutative rings, using the sup norm.

                      Equations
                      • Pi.seminormedCommRing = let __src := Pi.nonUnitalSeminormedCommRing; let __src_1 := Pi.ring; SeminormedCommRing.mk
                      Equations
                      • MulOpposite.instSeminormedCommRing = let __spread.0 := MulOpposite.instSeminormedRing; let __spread.1 := MulOpposite.instNonUnitalSeminormedCommRing; SeminormedCommRing.mk
                      instance Subalgebra.seminormedCommRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [SeminormedCommRing E] [Algebra 𝕜 E] (s : Subalgebra 𝕜 E) :

                      A subalgebra of a seminormed commutative ring is also a seminormed commutative ring, with the restriction of the norm.

                      Equations
                      instance Subalgebra.normedCommRing {𝕜 : Type u_5} [CommRing 𝕜] {E : Type u_6} [NormedCommRing E] [Algebra 𝕜 E] (s : Subalgebra 𝕜 E) :

                      A subalgebra of a normed commutative ring is also a normed commutative ring, with the restriction of the norm.

                      Equations
                      • s.normedCommRing = let __src := s.seminormedCommRing; let __src_1 := s.normedRing; NormedCommRing.mk
                      Equations
                      • ULift.normedCommRing = let __src := ULift.normedRing; let __src_1 := ULift.seminormedCommRing; NormedCommRing.mk
                      instance Prod.normedCommRing {α : Type u_1} {β : Type u_2} [NormedCommRing α] [NormedCommRing β] :

                      Normed commutative ring structure on the product of two normed commutative rings, using the sup norm.

                      Equations
                      • Prod.normedCommRing = let __src := Prod.nonUnitalNormedRing; let __src_1 := Prod.instCommRing; NormedCommRing.mk
                      instance Pi.normedCommutativeRing {ι : Type u_4} {π : ιType u_5} [Fintype ι] [(i : ι) → NormedCommRing (π i)] :
                      NormedCommRing ((i : ι) → π i)

                      Normed commutative ring structure on the product of finitely many normed commutative rings, using the sup norm.

                      Equations
                      • Pi.normedCommutativeRing = let __src := Pi.seminormedCommRing; let __src_1 := Pi.normedAddCommGroup; NormedCommRing.mk
                      Equations
                      • MulOpposite.instNormedCommRing = let __spread.0 := MulOpposite.instNormedRing; let __spread.1 := MulOpposite.instSeminormedCommRing; NormedCommRing.mk
                      @[instance 100]
                      Equations
                      • =
                      @[instance 100]

                      A seminormed ring is a topological ring.

                      Equations
                      • =
                      @[simp]
                      theorem norm_mul {α : Type u_1} [NormedDivisionRing α] (a : α) (b : α) :
                      @[instance 900]
                      Equations
                      • =
                      Equations
                      • =
                      @[simp]
                      theorem nnnorm_mul {α : Type u_1} [NormedDivisionRing α] (a : α) (b : α) :
                      @[simp]
                      theorem normHom_apply {α : Type u_1} [NormedDivisionRing α] :
                      ∀ (x : α), normHom x = x
                      def normHom {α : Type u_1} [NormedDivisionRing α] :

                      norm as a MonoidWithZeroHom.

                      Equations
                      • normHom = { toFun := fun (x : α) => x, map_zero' := , map_one' := , map_mul' := }
                      Instances For
                        @[simp]
                        theorem nnnormHom_apply {α : Type u_1} [NormedDivisionRing α] :
                        ∀ (x : α), nnnormHom x = x‖₊

                        nnnorm as a MonoidWithZeroHom.

                        Equations
                        • nnnormHom = { toFun := fun (x : α) => x‖₊, map_zero' := , map_one' := , map_mul' := }
                        Instances For
                          @[simp]
                          theorem norm_pow {α : Type u_1} [NormedDivisionRing α] (a : α) (n : ) :
                          a ^ n = a ^ n
                          @[simp]
                          theorem nnnorm_pow {α : Type u_1} [NormedDivisionRing α] (a : α) (n : ) :
                          theorem List.norm_prod {α : Type u_1} [NormedDivisionRing α] (l : List α) :
                          l.prod = (List.map norm l).prod
                          theorem List.nnnorm_prod {α : Type u_1} [NormedDivisionRing α] (l : List α) :
                          l.prod‖₊ = (List.map nnnorm l).prod
                          @[simp]
                          theorem norm_div {α : Type u_1} [NormedDivisionRing α] (a : α) (b : α) :
                          @[simp]
                          theorem nnnorm_div {α : Type u_1} [NormedDivisionRing α] (a : α) (b : α) :
                          @[simp]
                          theorem norm_inv {α : Type u_1} [NormedDivisionRing α] (a : α) :
                          @[simp]
                          theorem nnnorm_inv {α : Type u_1} [NormedDivisionRing α] (a : α) :
                          @[simp]
                          theorem norm_zpow {α : Type u_1} [NormedDivisionRing α] (a : α) (n : ) :
                          a ^ n = a ^ n
                          @[simp]
                          theorem nnnorm_zpow {α : Type u_1} [NormedDivisionRing α] (a : α) (n : ) :
                          theorem dist_inv_inv₀ {α : Type u_1} [NormedDivisionRing α] {z : α} {w : α} (hz : z 0) (hw : w 0) :
                          theorem nndist_inv_inv₀ {α : Type u_1} [NormedDivisionRing α] {z : α} {w : α} (hz : z 0) (hw : w 0) :
                          theorem antilipschitzWith_mul_left {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a 0) :
                          AntilipschitzWith a‖₊⁻¹ fun (x : α) => a * x
                          theorem antilipschitzWith_mul_right {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a 0) :
                          AntilipschitzWith a‖₊⁻¹ fun (x : α) => x * a
                          @[simp]
                          theorem DilationEquiv.mulLeft_symm_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a 0) (x : α) :
                          (DilationEquiv.mulLeft a ha).symm x = a⁻¹ * x
                          @[simp]
                          theorem DilationEquiv.mulLeft_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a 0) (x : α) :
                          def DilationEquiv.mulLeft {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a 0) :
                          α ≃ᵈ α

                          Multiplication by a nonzero element a on the left as a DilationEquiv of a normed division ring.

                          Equations
                          Instances For
                            @[simp]
                            theorem DilationEquiv.mulRight_symm_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a 0) (x : α) :
                            (DilationEquiv.mulRight a ha).symm x = x * a⁻¹
                            @[simp]
                            theorem DilationEquiv.mulRight_apply {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a 0) (x : α) :
                            def DilationEquiv.mulRight {α : Type u_1} [NormedDivisionRing α] (a : α) (ha : a 0) :
                            α ≃ᵈ α

                            Multiplication by a nonzero element a on the right as a DilationEquiv of a normed division ring.

                            Equations
                            Instances For
                              @[simp]
                              theorem Filter.comap_mul_left_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a 0) :
                              @[simp]
                              theorem Filter.map_mul_left_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a 0) :
                              Filter.map (fun (x : α) => a * x) (Bornology.cobounded α) = Bornology.cobounded α
                              @[simp]
                              theorem Filter.comap_mul_right_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a 0) :
                              @[simp]
                              theorem Filter.map_mul_right_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a 0) :
                              Filter.map (fun (x : α) => x * a) (Bornology.cobounded α) = Bornology.cobounded α
                              theorem Filter.tendsto_mul_left_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a 0) :

                              Multiplication on the left by a nonzero element of a normed division ring tends to infinity at infinity.

                              theorem Filter.tendsto_mul_right_cobounded {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : a 0) :

                              Multiplication on the right by a nonzero element of a normed division ring tends to infinity at infinity.

                              @[instance 100]
                              Equations
                              • =
                              @[instance 100]

                              A normed division ring is a topological division ring.

                              Equations
                              • =
                              theorem IsOfFinOrder.norm_eq_one {α : Type u_1} [NormedDivisionRing α] {a : α} (ha : IsOfFinOrder a) :
                              class NormedField (α : Type u_5) extends Norm , Field , MetricSpace :
                              Type u_5

                              A normed field is a field with a norm satisfying ‖x y‖ = ‖x‖ ‖y‖.

                              Instances
                                theorem NormedField.dist_eq {α : Type u_5} [self : NormedField α] (x : α) (y : α) :
                                dist x y = x - y

                                The distance is induced by the norm.

                                theorem NormedField.norm_mul' {α : Type u_5} [self : NormedField α] (a : α) (b : α) :

                                The norm is multiplicative.

                                class NontriviallyNormedField (α : Type u_5) extends NormedField :
                                Type u_5

                                A nontrivially normed field is a normed field in which there is an element of norm different from 0 and 1. This makes it possible to bring any element arbitrarily close to 0 by multiplication by the powers of any element, and thus to relate algebra and topology.

                                Instances
                                  theorem NontriviallyNormedField.non_trivial {α : Type u_5} [self : NontriviallyNormedField α] :
                                  ∃ (x : α), 1 < x

                                  The norm attains a value exceeding 1.

                                  class DenselyNormedField (α : Type u_5) extends NormedField :
                                  Type u_5

                                  A densely normed field is a normed field for which the image of the norm is dense in ℝ≥0, which means it is also nontrivially normed. However, not all nontrivally normed fields are densely normed; in particular, the Padics exhibit this fact.

                                  Instances
                                    theorem DenselyNormedField.lt_norm_lt {α : Type u_5} [self : DenselyNormedField α] (x : ) (y : ) :
                                    0 xx < y∃ (a : α), x < a a < y

                                    The range of the norm is dense in the collection of nonnegative real numbers.

                                    @[instance 100]

                                    A densely normed field is always a nontrivially normed field. See note [lower instance priority].

                                    Equations
                                    @[instance 100]
                                    Equations
                                    @[instance 100]
                                    Equations
                                    @[simp]
                                    theorem norm_prod {α : Type u_1} {β : Type u_2} [NormedField α] (s : Finset β) (f : βα) :
                                    bs, f b = bs, f b
                                    @[simp]
                                    theorem nnnorm_prod {α : Type u_1} {β : Type u_2} [NormedField α] (s : Finset β) (f : βα) :
                                    bs, f b‖₊ = bs, f b‖₊
                                    theorem NormedField.exists_lt_norm (α : Type u_1) [NontriviallyNormedField α] (r : ) :
                                    ∃ (x : α), r < x
                                    theorem NormedField.exists_norm_lt (α : Type u_1) [NontriviallyNormedField α] {r : } (hr : 0 < r) :
                                    ∃ (x : α), 0 < x x < r
                                    theorem NormedField.exists_lt_norm_lt (α : Type u_1) [DenselyNormedField α] {r₁ : } {r₂ : } (h₀ : 0 r₁) (h : r₁ < r₂) :
                                    ∃ (x : α), r₁ < x x < r₂
                                    theorem NormedField.exists_lt_nnnorm_lt (α : Type u_1) [DenselyNormedField α] {r₁ : NNReal} {r₂ : NNReal} (h : r₁ < r₂) :
                                    ∃ (x : α), r₁ < x‖₊ x‖₊ < r₂
                                    def NontriviallyNormedField.ofNormNeOne {𝕜 : Type u_5} [h' : NormedField 𝕜] (h : ∃ (x : 𝕜), x 0 x 1) :

                                    A normed field is nontrivially normed provided that the norm of some nonzero element is not one.

                                    Equations
                                    Instances For
                                      noncomputable instance Real.normedField :
                                      Equations
                                      theorem Real.toNNReal_mul_nnnorm {x : } (y : ) (hx : 0 x) :
                                      x.toNNReal * y‖₊ = x * y‖₊
                                      theorem Real.nnnorm_mul_toNNReal (x : ) {y : } (hy : 0 y) :
                                      x‖₊ * y.toNNReal = x * y‖₊
                                      theorem NNReal.norm_eq (x : NNReal) :
                                      x = x
                                      @[simp]
                                      theorem NNReal.nnnorm_eq (x : NNReal) :
                                      x‖₊ = x
                                      @[simp]
                                      theorem norm_norm {α : Type u_1} [SeminormedAddCommGroup α] (x : α) :
                                      @[simp]
                                      theorem NormedAddCommGroup.tendsto_atTop {α : Type u_1} [Nonempty α] [SemilatticeSup α] {β : Type u_5} [SeminormedAddCommGroup β] {f : αβ} {b : β} :
                                      Filter.Tendsto f Filter.atTop (nhds b) ∀ (ε : ), 0 < ε∃ (N : α), ∀ (n : α), N nf n - b < ε

                                      A restatement of MetricSpace.tendsto_atTop in terms of the norm.

                                      theorem NormedAddCommGroup.tendsto_atTop' {α : Type u_1} [Nonempty α] [SemilatticeSup α] [NoMaxOrder α] {β : Type u_5} [SeminormedAddCommGroup β] {f : αβ} {b : β} :
                                      Filter.Tendsto f Filter.atTop (nhds b) ∀ (ε : ), 0 < ε∃ (N : α), ∀ (n : α), N < nf n - b < ε

                                      A variant of NormedAddCommGroup.tendsto_atTop that uses ∃ N, ∀ n > N, ... rather than ∃ N, ∀ n ≥ N, ...

                                      class RingHomIsometric {R₁ : Type u_5} {R₂ : Type u_6} [Semiring R₁] [Semiring R₂] [Norm R₁] [Norm R₂] (σ : R₁ →+* R₂) :

                                      This class states that a ring homomorphism is isometric. This is a sufficient assumption for a continuous semilinear map to be bounded and this is the main use for this typeclass.

                                      • is_iso : ∀ {x : R₁}, σ x = x

                                        The ring homomorphism is an isometry.

                                      Instances
                                        @[simp]
                                        theorem RingHomIsometric.is_iso {R₁ : Type u_5} {R₂ : Type u_6} [Semiring R₁] [Semiring R₂] [Norm R₁] [Norm R₂] {σ : R₁ →+* R₂} [self : RingHomIsometric σ] {x : R₁} :

                                        The ring homomorphism is an isometry.

                                        Equations
                                        • =

                                        Induced normed structures #

                                        @[reducible, inline]

                                        A non-unital ring homomorphism from a NonUnitalRing to a NonUnitalSeminormedRing induces a NonUnitalSeminormedRing structure on the domain.

                                        See note [reducible non-instances]

                                        Equations
                                        Instances For
                                          @[reducible, inline]
                                          abbrev NonUnitalNormedRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [NonUnitalRing R] [NonUnitalNormedRing S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective f) :

                                          An injective non-unital ring homomorphism from a NonUnitalRing to a NonUnitalNormedRing induces a NonUnitalNormedRing structure on the domain.

                                          See note [reducible non-instances]

                                          Equations
                                          Instances For
                                            @[reducible, inline]
                                            abbrev SeminormedRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [Ring R] [SeminormedRing S] [NonUnitalRingHomClass F R S] (f : F) :

                                            A non-unital ring homomorphism from a Ring to a SeminormedRing induces a SeminormedRing structure on the domain.

                                            See note [reducible non-instances]

                                            Equations
                                            Instances For
                                              @[reducible, inline]
                                              abbrev NormedRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [Ring R] [NormedRing S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective f) :

                                              An injective non-unital ring homomorphism from a Ring to a NormedRing induces a NormedRing structure on the domain.

                                              See note [reducible non-instances]

                                              Equations
                                              Instances For
                                                @[reducible, inline]

                                                A non-unital ring homomorphism from a NonUnitalCommRing to a NonUnitalSeminormedCommRing induces a NonUnitalSeminormedCommRing structure on the domain.

                                                See note [reducible non-instances]

                                                Equations
                                                Instances For
                                                  @[reducible, inline]

                                                  An injective non-unital ring homomorphism from a NonUnitalCommRing to a NonUnitalNormedCommRing induces a NonUnitalNormedCommRing structure on the domain.

                                                  See note [reducible non-instances]

                                                  Equations
                                                  Instances For
                                                    @[reducible, inline]
                                                    abbrev SeminormedCommRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [CommRing R] [SeminormedRing S] [NonUnitalRingHomClass F R S] (f : F) :

                                                    A non-unital ring homomorphism from a CommRing to a SeminormedRing induces a SeminormedCommRing structure on the domain.

                                                    See note [reducible non-instances]

                                                    Equations
                                                    Instances For
                                                      @[reducible, inline]
                                                      abbrev NormedCommRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [CommRing R] [NormedRing S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective f) :

                                                      An injective non-unital ring homomorphism from a CommRing to a NormedRing induces a NormedCommRing structure on the domain.

                                                      See note [reducible non-instances]

                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]
                                                        abbrev NormedDivisionRing.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [DivisionRing R] [NormedDivisionRing S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective f) :

                                                        An injective non-unital ring homomorphism from a DivisionRing to a NormedRing induces a NormedDivisionRing structure on the domain.

                                                        See note [reducible non-instances]

                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]
                                                          abbrev NormedField.induced {F : Type u_5} (R : Type u_6) (S : Type u_7) [FunLike F R S] [Field R] [NormedField S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective f) :

                                                          An injective non-unital ring homomorphism from a Field to a NormedRing induces a NormedField structure on the domain.

                                                          See note [reducible non-instances]

                                                          Equations
                                                          Instances For
                                                            theorem NormOneClass.induced {F : Type u_8} (R : Type u_9) (S : Type u_10) [Ring R] [SeminormedRing S] [NormOneClass S] [FunLike F R S] [RingHomClass F R S] (f : F) :

                                                            A ring homomorphism from a Ring R to a SeminormedRing S which induces the norm structure SeminormedRing.induced makes R satisfy ‖(1 : R)‖ = 1 whenever ‖(1 : S)‖ = 1.

                                                            instance SubringClass.toNormedRing {S : Type u_5} {R : Type u_6} [SetLike S R] [NormedRing R] [SubringClass S R] (s : S) :
                                                            Equations