Documentation

Mathlib.Analysis.Normed.Ring.Basic

Normed rings #

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

A normed ring instance can be constructed from a given real absolute value on a ring via AbsoluteValue.toNormedRing.

class NonUnitalSeminormedRing (α : Type u_5) extends Norm α, NonUnitalRing α, PseudoMetricSpace α :
Type u_5

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

Instances
    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
      @[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
          @[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
              @[instance 100]
              instance NormedRing.toSeminormedRing {α : Type u_2} [β : 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

                    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
                      @[instance 100]

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

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

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

                        Instances
                          class NormedCommRing (α : Type u_5) extends NormedRing α, CommRing α :
                          Type u_5

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

                          Instances
                            @[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]
                                    @[simp]
                                    theorem enorm_one {G : Type u_1} [SeminormedAddCommGroup G] [One G] [NormOneClass G] :
                                    @[instance 100]
                                    Equations
                                      instance Prod.normOneClass {α : Type u_2} {β : Type u_3} [SeminormedAddCommGroup α] [One α] [NormOneClass α] [SeminormedAddCommGroup β] [One β] [NormOneClass β] :
                                      instance Pi.normOneClass {ι : Type u_5} {α : ιType u_6} [Nonempty ι] [Fintype ι] [(i : ι) → SeminormedAddCommGroup (α i)] [(i : ι) → One (α i)] [∀ (i : ι), NormOneClass (α i)] :
                                      NormOneClass ((i : ι) → α i)
                                      theorem norm_mul_le {α : Type u_2} [NonUnitalSeminormedRing α] (a b : α) :

                                      The norm is submultiplicative.

                                      theorem norm_mul_le_of_le {α : Type u_2} [NonUnitalSeminormedRing α] {a₁ a₂ : α} {r₁ r₂ : } (h₁ : a₁ r₁) (h₂ : a₂ r₂) :
                                      a₁ * a₂ r₁ * r₂
                                      theorem nnnorm_mul_le_of_le {α : Type u_2} [NonUnitalSeminormedRing α] {a₁ a₂ : α} {r₁ r₂ : NNReal} (h₁ : a₁‖₊ r₁) (h₂ : a₂‖₊ r₂) :
                                      a₁ * a₂‖₊ r₁ * r₂
                                      theorem norm_mul₃_le {α : Type u_2} [NonUnitalSeminormedRing α] {a b c : α} :
                                      theorem one_le_norm_one (β : Type u_5) [NormedRing β] [Nontrivial β] :

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

                                      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
                                        @[instance 75]
                                        instance NonUnitalSubalgebraClass.nonUnitalSeminormedRing {S : Type u_5} {𝕜 : Type u_6} {E : Type u_7} [CommRing 𝕜] [NonUnitalSeminormedRing E] [Module 𝕜 E] [SetLike S E] [NonUnitalSubringClass S E] [SMulMemClass S 𝕜 E] (s : S) :

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

                                        Equations

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

                                          Equations
                                            @[instance 75]
                                            instance NonUnitalSubalgebraClass.nonUnitalNormedRing {S : Type u_5} {𝕜 : Type u_6} {E : Type u_7} [CommRing 𝕜] [NonUnitalNormedRing E] [Module 𝕜 E] [SetLike S E] [NonUnitalSubringClass S E] [SMulMemClass S 𝕜 E] (s : S) :

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

                                            Equations

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

                                              Equations
                                                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
                                                  @[instance 75]
                                                  instance SubalgebraClass.seminormedRing {S : Type u_5} {𝕜 : Type u_6} {E : Type u_7} [CommRing 𝕜] [SeminormedRing E] [Algebra 𝕜 E] [SetLike S E] [SubringClass S E] [SMulMemClass S 𝕜 E] (s : S) :

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

                                                  Equations
                                                    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
                                                      @[instance 75]
                                                      instance SubalgebraClass.normedRing {S : Type u_5} {𝕜 : Type u_6} {E : Type u_7} [CommRing 𝕜] [NormedRing E] [Algebra 𝕜 E] [SetLike S E] [SubringClass S E] [SMulMemClass S 𝕜 E] (s : S) :

                                                      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_2} [SeminormedRing α] (n : ) :
                                                        n n * 1
                                                        theorem List.norm_prod_le' {α : Type u_2} [SeminormedRing α] {l : List α} :
                                                        theorem List.nnnorm_prod_le' {α : Type u_2} [SeminormedRing α] {l : List α} (hl : l []) :
                                                        theorem List.norm_prod_le {α : Type u_2} [SeminormedRing α] [NormOneClass α] (l : List α) :
                                                        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_2} [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_2} [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_2} [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_2} [SeminormedRing α] [NormOneClass α] (a : α) (n : ) :

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

                                                        instance Prod.seminormedRing {α : Type u_2} {β : Type u_3} [SeminormedRing α] [SeminormedRing β] :

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

                                                        Equations
                                                          theorem norm_sub_mul_le {α : Type u_2} [SeminormedRing α] {a b c : α} (ha : a 1) :
                                                          c - a * b c - a + 1 - b

                                                          This inequality is particularly useful when c = 1 and ‖a‖ = ‖b‖ = 1 as it then shows that chord length is a metric on the unit complex numbers.

                                                          theorem norm_sub_mul_le' {α : Type u_2} [SeminormedRing α] {a b c : α} (hb : b 1) :
                                                          c - a * b 1 - a + c - b

                                                          This inequality is particularly useful when c = 1 and ‖a‖ = ‖b‖ = 1 as it then shows that chord length is a metric on the unit complex numbers.

                                                          theorem nnnorm_sub_mul_le {α : Type u_2} [SeminormedRing α] {a b c : α} (ha : a‖₊ 1) :

                                                          This inequality is particularly useful when c = 1 and ‖a‖ = ‖b‖ = 1 as it then shows that chord length is a metric on the unit complex numbers.

                                                          theorem nnnorm_sub_mul_le' {α : Type u_2} [SeminormedRing α] {a b c : α} (hb : b‖₊ 1) :

                                                          This inequality is particularly useful when c = 1 and ‖a‖ = ‖b‖ = 1 as it then shows that chord length is a metric on the unit complex numbers.

                                                          theorem norm_commutator_units_sub_one_le {α : Type u_2} [SeminormedRing α] (a b : αˣ) :
                                                          ↑(a * b * a⁻¹ * b⁻¹) - 1 2 * a⁻¹ * b⁻¹ * a - 1 * b - 1
                                                          def RingHom.IsBounded {α : Type u_5} [SeminormedRing α] {β : Type u_6} [SeminormedRing β] (f : α →+* β) :

                                                          A homomorphism f between semi_normed_rings is bounded if there exists a positive constant C such that for all x in α, norm (f x) ≤ C * norm x.

                                                          Equations
                                                            Instances For

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

                                                              Equations
                                                                theorem Units.norm_pos {α : Type u_2} [NormedRing α] [Nontrivial α] (x : αˣ) :
                                                                0 < x
                                                                theorem Units.nnnorm_pos {α : Type u_2} [NormedRing α] [Nontrivial α] (x : αˣ) :
                                                                0 < x‖₊
                                                                Equations
                                                                  instance Prod.normedRing {α : Type u_2} {β : Type u_3} [NormedRing α] [NormedRing β] :
                                                                  NormedRing (α × β)

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

                                                                  Equations

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

                                                                    Equations

                                                                      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

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

                                                                          Equations

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

                                                                            Equations
                                                                              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
                                                                                  instance Prod.normedCommRing {α : Type u_2} {β : Type u_3} [NormedCommRing α] [NormedCommRing β] :

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

                                                                                  Equations
                                                                                    theorem IsPowMul.restriction {R : Type u_5} {S : Type u_6} [CommRing R] [Ring S] [Algebra R S] (A : Subalgebra R S) {f : S} (hf_pm : IsPowMul f) :
                                                                                    IsPowMul fun (x : A) => f x

                                                                                    The restriction of a power-multiplicative function to a subalgebra is power-multiplicative.

                                                                                    theorem NNReal.norm_eq (x : NNReal) :
                                                                                    x = x
                                                                                    @[simp]
                                                                                    theorem NNReal.nnnorm_eq (x : NNReal) :
                                                                                    x‖₊ = x
                                                                                    @[simp]
                                                                                    theorem NNReal.enorm_eq (x : NNReal) :
                                                                                    x‖ₑ = x
                                                                                    theorem NormedAddCommGroup.tendsto_atTop {α : Type u_2} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {β : 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_2} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [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
                                                                                      class NormMulClass (α : Type u_5) [Norm α] [Mul α] :

                                                                                      A mixin class for strict multiplicativity of the norm, ‖a * b‖ = ‖a‖ * ‖b‖ (rather than as in the definition of NormedRing). Many NormedRings satisfy this stronger property, including all NormedDivisionRings and NormedFields.

                                                                                      Instances
                                                                                        @[simp]
                                                                                        theorem norm_mul {α : Type u_2} [Norm α] [Mul α] [NormMulClass α] (a b : α) :
                                                                                        @[simp]
                                                                                        theorem nnnorm_mul {α : Type u_2} [SeminormedAddCommGroup α] [Mul α] [NormMulClass α] (a b : α) :
                                                                                        @[simp]
                                                                                        theorem enorm_mul {α : Type u_2} [SeminormedAddCommGroup α] [Mul α] [NormMulClass α] (a b : α) :
                                                                                        def normHom {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] :

                                                                                        norm as a MonoidWithZeroHom.

                                                                                        Equations
                                                                                          Instances For
                                                                                            @[simp]
                                                                                            theorem normHom_apply {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (x✝ : α) :
                                                                                            normHom x✝ = x✝

                                                                                            nnnorm as a MonoidWithZeroHom.

                                                                                            Equations
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                theorem nnnormHom_apply {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (x✝ : α) :
                                                                                                @[simp]
                                                                                                theorem norm_pow {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (a : α) (n : ) :
                                                                                                a ^ n = a ^ n
                                                                                                @[simp]
                                                                                                theorem nnnorm_pow {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (a : α) (n : ) :
                                                                                                @[simp]
                                                                                                theorem enorm_pow {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (a : α) (n : ) :
                                                                                                theorem List.norm_prod {α : Type u_2} [SeminormedRing α] [NormOneClass α] [NormMulClass α] (l : List α) :
                                                                                                @[simp]
                                                                                                theorem norm_prod {α : Type u_2} {β : Type u_3} [SeminormedCommRing α] [NormMulClass α] [NormOneClass α] (s : Finset β) (f : βα) :
                                                                                                bs, f b = bs, f b
                                                                                                @[simp]
                                                                                                theorem nnnorm_prod {α : Type u_2} {β : Type u_3} [SeminormedCommRing α] [NormMulClass α] [NormOneClass α] (s : Finset β) (f : βα) :
                                                                                                bs, f b‖₊ = bs, f b‖₊

                                                                                                Deduce NormOneClass from NormMulClass under a suitable nontriviality hypothesis. Not an instance, in order to avoid loops with NormOneClass.nontrivial.

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

                                                                                                                                theorem NormMulClass.induced {F : Type u_8} (R : Type u_9) (S : Type u_10) [Ring R] [SeminormedRing S] [NormMulClass 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.toSeminormedRing {S : Type u_5} {R : Type u_6} [SetLike S R] [SeminormedRing R] [SubringClass S R] (s : S) :
                                                                                                                                Equations
                                                                                                                                  instance SubringClass.toNormedRing {S : Type u_5} {R : Type u_6} [SetLike S R] [NormedRing R] [SubringClass S R] (s : S) :
                                                                                                                                  Equations
                                                                                                                                    instance SubringClass.toSeminormedCommRing {S : Type u_5} {R : Type u_6} [SetLike S R] [SeminormedCommRing R] [_h : SubringClass S R] (s : S) :
                                                                                                                                    Equations
                                                                                                                                      instance SubringClass.toNormedCommRing {S : Type u_5} {R : Type u_6} [SetLike S R] [NormedCommRing R] [SubringClass S R] (s : S) :
                                                                                                                                      Equations
                                                                                                                                        instance SubringClass.toNormOneClass {S : Type u_5} {R : Type u_6} [SetLike S R] [SeminormedRing R] [NormOneClass R] [SubringClass S R] (s : S) :
                                                                                                                                        instance SubringClass.toNormMulClass {S : Type u_5} {R : Type u_6} [SetLike S R] [SeminormedRing R] [NormMulClass R] [SubringClass S R] (s : S) :
                                                                                                                                        noncomputable def AbsoluteValue.toNormedRing {R : Type u_5} [Ring R] (v : AbsoluteValue R ) :

                                                                                                                                        A real absolute value on a ring determines a NormedRing structure.

                                                                                                                                        Equations
                                                                                                                                          Instances For