# mathlibdocumentation

analysis.normed.field.basic

# Normed fields #

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

@[class]
structure non_unital_semi_normed_ring (α : Type u_5) :
Type u_5
• to_has_norm :
• to_non_unital_ring :
• to_pseudo_metric_space :
• dist_eq : ∀ (x y : α), = x - y
• norm_mul : ∀ (a b : α), a * b a * b

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

Instances of this typeclass
Instances of other typeclasses for non_unital_semi_normed_ring
• non_unital_semi_normed_ring.has_sizeof_inst
@[class]
structure semi_normed_ring (α : Type u_5) :
Type u_5

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

Instances of this typeclass
Instances of other typeclasses for semi_normed_ring
• semi_normed_ring.has_sizeof_inst
@[protected, instance]

A seminormed ring is a non-unital seminormed ring.

Equations
@[class]
structure non_unital_normed_ring (α : Type u_5) :
Type u_5
• to_has_norm :
• to_non_unital_ring :
• to_metric_space :
• dist_eq : ∀ (x y : α), = x - y
• norm_mul : ∀ (a b : α), a * b a * b

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

Instances of this typeclass
Instances of other typeclasses for non_unital_normed_ring
• non_unital_normed_ring.has_sizeof_inst
@[protected, instance]

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

Equations
@[class]
structure normed_ring (α : Type u_5) :
Type u_5

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

Instances of this typeclass
Instances of other typeclasses for normed_ring
• normed_ring.has_sizeof_inst
@[class]
structure normed_division_ring (α : Type u_5) :
Type u_5
• to_has_norm :
• to_division_ring :
• to_metric_space :
• dist_eq : ∀ (x y : α), = x - y
• norm_mul' : ∀ (a b : α), a * b = a * b

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

Instances of this typeclass
Instances of other typeclasses for normed_division_ring
• normed_division_ring.has_sizeof_inst
@[protected, instance]

A normed division ring is a normed ring.

Equations
@[protected, instance]
def normed_ring.to_semi_normed_ring {α : Type u_1} [β : normed_ring α] :

A normed ring is a seminormed ring.

Equations
@[protected, instance]
def normed_ring.to_non_unital_normed_ring {α : Type u_1} [β : normed_ring α] :

A normed ring is a non-unital normed ring.

Equations
@[class]
structure semi_normed_comm_ring (α : Type u_5) :
Type u_5
• to_semi_normed_ring :
• mul_comm : ∀ (x y : α), x * y = y * x

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

Instances of this typeclass
Instances of other typeclasses for semi_normed_comm_ring
• semi_normed_comm_ring.has_sizeof_inst
@[class]
structure normed_comm_ring (α : Type u_5) :
Type u_5
• to_normed_ring :
• mul_comm : ∀ (x y : α), x * y = y * x

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

Instances of this typeclass
Instances of other typeclasses for normed_comm_ring
• normed_comm_ring.has_sizeof_inst
@[protected, instance]

A normed commutative ring is a seminormed commutative ring.

Equations
@[protected, instance]
Equations
@[class]
structure norm_one_class (α : Type u_5) [has_norm α] [has_one α] :
Prop

A mixin class with the axiom ∥1∥ = 1. Many normed_rings and all normed_fields satisfy this axiom.

Instances of this typeclass
@[simp]
theorem nnnorm_one {α : Type u_1} [has_one α]  :
theorem norm_one_class.nontrivial (α : Type u_1) [has_one α]  :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def ulift.norm_one_class {α : Type u_1} [has_one α]  :
@[protected, instance]
def prod.norm_one_class {α : Type u_1} {β : Type u_2} [has_one α] [has_one β]  :
@[protected, instance]
def pi.norm_one_class {ι : Type u_1} {α : ι → Type u_2} [nonempty ι] [fintype ι] [Π (i : ι), ] [Π (i : ι), has_one (α i)] [∀ (i : ι), norm_one_class (α i)] :
norm_one_class (Π (i : ι), α i)
theorem norm_mul_le {α : Type u_1} (a b : α) :
theorem nnnorm_mul_le {α : Type u_1} (a b : α) :
theorem one_le_norm_one (β : Type u_1) [normed_ring β] [nontrivial β] :
theorem one_le_nnnorm_one (β : Type u_1) [normed_ring β] [nontrivial β] :
theorem filter.tendsto.zero_mul_is_bounded_under_le {α : Type u_1} {ι : Type u_4} {f g : ι → α} {l : filter ι} (hf : (nhds 0)) (hg : ) :
filter.tendsto (λ (x : ι), f x * g x) l (nhds 0)
theorem filter.is_bounded_under_le.mul_tendsto_zero {α : Type u_1} {ι : Type u_4} {f g : ι → α} {l : filter ι} (hf : ) (hg : (nhds 0)) :
filter.tendsto (λ (x : ι), f x * g x) l (nhds 0)
theorem mul_left_bound {α : Type u_1} (x y : α) :

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

theorem mul_right_bound {α : Type u_1} (x y : α) :

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

@[protected, instance]
def ulift.non_unital_semi_normed_ring {α : Type u_1}  :
Equations
@[protected, instance]
noncomputable def prod.non_unital_semi_normed_ring {α : Type u_1} {β : Type u_2}  :

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

Equations
@[protected, instance]
noncomputable def pi.non_unital_semi_normed_ring {ι : Type u_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), ] :
non_unital_semi_normed_ring (Π (i : ι), π i)

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

Equations
@[protected, instance]
def subalgebra.semi_normed_ring {𝕜 : Type u_1} {_x : comm_ring 𝕜} {E : Type u_2} {_x_1 : E} (s : E) :

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

Equations
@[protected, instance]
def subalgebra.normed_ring {𝕜 : Type u_1} {_x : comm_ring 𝕜} {E : Type u_2} [normed_ring E] {_x_1 : E} (s : 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} (n : ) :
theorem list.norm_prod_le' {α : Type u_1} {l : list α} :
l.prod
theorem list.nnnorm_prod_le' {α : Type u_1} {l : list α} (hl : l list.nil) :
theorem list.norm_prod_le {α : Type u_1} (l : list α) :
theorem list.nnnorm_prod_le {α : Type u_1} (l : list α) :
theorem finset.norm_prod_le' {ι : Type u_4} {α : Type u_1} (s : finset ι) (hs : s.nonempty) (f : ι → α) :
s.prod (λ (i : ι), f i) s.prod (λ (i : ι), f i)
theorem finset.nnnorm_prod_le' {ι : Type u_4} {α : Type u_1} (s : finset ι) (hs : s.nonempty) (f : ι → α) :
s.prod (λ (i : ι), f i)∥₊ s.prod (λ (i : ι), f i∥₊)
theorem finset.norm_prod_le {ι : Type u_4} {α : Type u_1} (s : finset ι) (f : ι → α) :
s.prod (λ (i : ι), f i) s.prod (λ (i : ι), f i)
theorem finset.nnnorm_prod_le {ι : Type u_4} {α : Type u_1} (s : finset ι) (f : ι → α) :
s.prod (λ (i : ι), f i)∥₊ s.prod (λ (i : ι), f i∥₊)
theorem nnnorm_pow_le' {α : Type u_1} (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} (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} (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} (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} (a : α) :
∀ᶠ (n : ) in filter.at_top, a ^ n a ^ n
@[protected, instance]
def ulift.semi_normed_ring {α : Type u_1}  :
Equations
@[protected, instance]
noncomputable def prod.semi_normed_ring {α : Type u_1} {β : Type u_2}  :

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

Equations
@[protected, instance]
noncomputable def pi.semi_normed_ring {ι : Type u_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), semi_normed_ring (π i)] :
semi_normed_ring (Π (i : ι), π i)

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

Equations
@[protected, instance]
def ulift.non_unital_normed_ring {α : Type u_1}  :
Equations
@[protected, instance]
noncomputable def prod.non_unital_normed_ring {α : Type u_1} {β : Type u_2}  :

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

Equations
@[protected, instance]
noncomputable def pi.non_unital_normed_ring {ι : Type u_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), ] :
non_unital_normed_ring (Π (i : ι), π i)

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

Equations
theorem units.norm_pos {α : Type u_1} [normed_ring α] [nontrivial α] (x : αˣ) :
theorem units.nnnorm_pos {α : Type u_1} [normed_ring α] [nontrivial α] (x : αˣ) :
@[protected, instance]
def ulift.normed_ring {α : Type u_1} [normed_ring α] :
Equations
@[protected, instance]
noncomputable def prod.normed_ring {α : Type u_1} {β : Type u_2} [normed_ring α] [normed_ring β] :
normed_ring × β)

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

Equations
@[protected, instance]
noncomputable def pi.normed_ring {ι : Type u_4} {π : ι → Type u_1} [fintype ι] [Π (i : ι), normed_ring (π i)] :
normed_ring (Π (i : ι), π i)

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

Equations
@[protected, instance]
def semi_normed_ring_top_monoid {α : Type u_1}  :
@[protected, instance]
def semi_normed_top_ring {α : Type u_1}  :

A seminormed ring is a topological ring.

@[simp]
theorem norm_mul {α : Type u_1} (a b : α) :
@[protected, instance]
def normed_division_ring.to_norm_one_class {α : Type u_1}  :
@[simp]
theorem nnnorm_mul {α : Type u_1} (a b : α) :
@[simp]
theorem norm_hom_apply {α : Type u_1} (ᾰ : α) :
=
def norm_hom {α : Type u_1}  :

norm as a monoid_with_zero_hom.

Equations
@[simp]
theorem nnnorm_hom_apply {α : Type u_1} (ᾰ : α) :
def nnnorm_hom {α : Type u_1}  :

nnnorm as a monoid_with_zero_hom.

Equations
@[simp]
theorem norm_pow {α : Type u_1} (a : α) (n : ) :
a ^ n = a ^ n
@[simp]
theorem nnnorm_pow {α : Type u_1} (a : α) (n : ) :
@[protected]
theorem list.norm_prod {α : Type u_1} (l : list α) :
@[protected]
theorem list.nnnorm_prod {α : Type u_1} (l : list α) :
@[simp]
theorem norm_div {α : Type u_1} (a b : α) :
@[simp]
theorem nnnorm_div {α : Type u_1} (a b : α) :
@[simp]
theorem norm_inv {α : Type u_1} (a : α) :
@[simp]
theorem nnnorm_inv {α : Type u_1} (a : α) :
@[simp]
theorem norm_zpow {α : Type u_1} (a : α) (n : ) :
a ^ n = a ^ n
@[simp]
theorem nnnorm_zpow {α : Type u_1} (a : α) (n : ) :
theorem filter.tendsto_mul_left_cobounded {α : Type u_1} {a : α} (ha : a 0) :

Multiplication on the left by a nonzero element of a normed division ring tends to infinity at infinity. TODO: use bornology.cobounded instead of filter.comap has_norm.norm filter.at_top.

theorem filter.tendsto_mul_right_cobounded {α : Type u_1} {a : α} (ha : a 0) :
filter.tendsto (λ (x : α), x * a)

Multiplication on the right by a nonzero element of a normed division ring tends to infinity at infinity. TODO: use bornology.cobounded instead of filter.comap has_norm.norm filter.at_top.

@[protected, instance]
@[class]
structure normed_field (α : Type u_5) :
Type u_5

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

Instances of this typeclass
Instances of other typeclasses for normed_field
• normed_field.has_sizeof_inst
@[class]
structure nontrivially_normed_field (α : Type u_5) :
Type u_5
• to_normed_field :
• non_trivial : ∃ (x : α), 1 < x

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 of this typeclass
Instances of other typeclasses for nontrivially_normed_field
• nontrivially_normed_field.has_sizeof_inst
@[class]
structure densely_normed_field (α : Type u_5) :
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 of this typeclass
Instances of other typeclasses for densely_normed_field
• densely_normed_field.has_sizeof_inst
@[protected, instance]

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

Equations
@[simp]
theorem norm_prod {α : Type u_1} {β : Type u_2} [normed_field α] (s : finset β) (f : β → α) :
s.prod (λ (b : β), f b) = s.prod (λ (b : β), f b)
@[simp]
theorem nnnorm_prod {α : Type u_1} {β : Type u_2} [normed_field α] (s : finset β) (f : β → α) :
s.prod (λ (b : β), f b)∥₊ = s.prod (λ (b : β), f b∥₊)
theorem normed_field.exists_one_lt_norm (α : Type u_1)  :
∃ (x : α), 1 < x
theorem normed_field.exists_lt_norm (α : Type u_1) (r : ) :
∃ (x : α), r < x
theorem normed_field.exists_norm_lt (α : Type u_1) {r : } (hr : 0 < r) :
∃ (x : α), 0 < x x < r
theorem normed_field.exists_norm_lt_one (α : Type u_1)  :
∃ (x : α), 0 < x x < 1
@[instance]
theorem normed_field.punctured_nhds_ne_bot {α : Type u_1} (x : α) :
{x}).ne_bot
@[instance]
theorem normed_field.nhds_within_is_unit_ne_bot {α : Type u_1}  :
{x : α | is_unit x}).ne_bot
theorem normed_field.exists_lt_norm_lt (α : Type u_1) {r₁ r₂ : } (h₀ : 0 r₁) (h : r₁ < r₂) :
∃ (x : α), r₁ < x x < r₂
theorem normed_field.exists_lt_nnnorm_lt (α : Type u_1) {r₁ r₂ : nnreal} (h : r₁ < r₂) :
∃ (x : α), r₁ < x∥₊ x∥₊ < r₂
@[protected, instance]
def normed_field.densely_ordered_range_norm (α : Type u_1)  :
@[protected, instance]
theorem normed_field.dense_range_nnnorm (α : Type u_1)  :
@[protected, instance]
noncomputable def real.normed_field  :
Equations
@[protected, instance]
noncomputable def real.densely_normed_field  :
Equations
theorem real.norm_of_nonneg {x : } (hx : 0 x) :
theorem real.norm_of_nonpos {x : } (hx : x 0) :
@[simp]
theorem real.norm_coe_nat (n : ) :
@[simp]
@[simp]
theorem real.norm_two  :
@[simp]
theorem real.nnnorm_two  :
theorem real.nnnorm_of_nonneg {x : } (hx : 0 x) :
x∥₊ = x, hx⟩
theorem real.ennnorm_eq_of_real {x : } (hx : 0 x) :
@[protected, instance]
def real.punctured_nhds_module_ne_bot {E : Type u_1} [nontrivial E] [ E] (x : E) :
{x}).ne_bot

If E is a nontrivial topological module over ℝ, then E has no isolated points. This is a particular case of module.punctured_nhds_ne_bot.

@[simp]
theorem nnreal.norm_eq (x : nnreal) :
@[simp]
theorem nnreal.nnnorm_eq (x : nnreal) :
@[simp]
theorem norm_norm {α : Type u_1} (x : α) :
@[simp]
theorem nnnorm_norm {α : Type u_1} (a : α) :
theorem normed_add_comm_group.tendsto_at_top {α : Type u_1} [nonempty α] {β : Type u_2} {f : α → β} {b : β} :
∀ (ε : ), 0 < ε(∃ (N : α), ∀ (n : α), N nf n - b < ε)

A restatement of metric_space.tendsto_at_top in terms of the norm.

theorem normed_add_comm_group.tendsto_at_top' {α : Type u_1} [nonempty α] [no_max_order α] {β : Type u_2} {f : α → β} {b : β} :
∀ (ε : ), 0 < ε(∃ (N : α), ∀ (n : α), N < nf n - b < ε)

A variant of normed_add_comm_group.tendsto_at_top that uses ∃ N, ∀ n > N, ... rather than ∃ N, ∀ n ≥ N, ...

@[protected, instance]
noncomputable def int.normed_comm_ring  :
Equations
@[norm_cast]
theorem int.norm_cast_real (m : ) :
theorem int.norm_eq_abs (n : ) :
@[protected, instance]
@[protected, instance]
noncomputable def rat.normed_field  :
Equations
@[protected, instance]
noncomputable def rat.densely_normed_field  :
Equations
@[simp, norm_cast]
theorem rat.norm_cast_real (r : ) :
@[simp, norm_cast]
theorem int.norm_cast_rat (m : ) :
theorem norm_nsmul_le {α : Type u_1} (n : ) (a : α) :
theorem norm_zsmul_le {α : Type u_1} (n : ) (a : α) :
theorem nnnorm_nsmul_le {α : Type u_1} (n : ) (a : α) :
theorem nnnorm_zsmul_le {α : Type u_1} (n : ) (a : α) :

## Multiplying two infinite sums in a normed ring #

In this section, we prove various results about (∑' x : ι, f x) * (∑' y : ι', g y) in a normed ring. There are similar results proven in topology/algebra/infinite_sum (e.g tsum_mul_tsum), but in a normed ring we get summability results which aren't true in general.

We first establish results about arbitrary index types, β and γ, and then we specialize to β = γ = ℕ to prove the Cauchy product formula (see tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm).

### Arbitrary index types #

theorem summable.mul_of_nonneg {ι : Type u_4} {ι' : Type u_5} {f : ι → } {g : ι' → } (hf : summable f) (hg : summable g) (hf' : 0 f) (hg' : 0 g) :
summable (λ (x : ι × ι'), f x.fst * g x.snd)
theorem summable.mul_norm {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [normed_ring α] {f : ι → α} {g : ι' → α} (hf : summable (λ (x : ι), f x)) (hg : summable (λ (x : ι'), g x)) :
summable (λ (x : ι × ι'), f x.fst * g x.snd)
theorem summable_mul_of_summable_norm {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [normed_ring α] {f : ι → α} {g : ι' → α} (hf : summable (λ (x : ι), f x)) (hg : summable (λ (x : ι'), g x)) :
summable (λ (x : ι × ι'), f x.fst * g x.snd)
theorem tsum_mul_tsum_of_summable_norm {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [normed_ring α] {f : ι → α} {g : ι' → α} (hf : summable (λ (x : ι), f x)) (hg : summable (λ (x : ι'), g x)) :
(∑' (x : ι), f x) * ∑' (y : ι'), g y = ∑' (z : ι × ι'), f z.fst * g z.snd

Product of two infinites sums indexed by arbitrary types. See also tsum_mul_tsum if f and g are not absolutely summable.

### ℕ-indexed families (Cauchy product) #

We prove two versions of the Cauchy product formula. The first one is tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm, where the n-th term is a sum over finset.range (n+1) involving nat substraction. In order to avoid nat substraction, we also provide tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm, where the n-th term is a sum over all pairs (k, l) such that k+l=n, which corresponds to the finset finset.nat.antidiagonal n.

theorem summable_norm_sum_mul_antidiagonal_of_summable_norm {α : Type u_1} [normed_ring α] {f g : → α} (hf : summable (λ (x : ), f x)) (hg : summable (λ (x : ), g x)) :
summable (λ (n : ), (λ (kl : × ), f kl.fst * g kl.snd))
theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm {α : Type u_1} [normed_ring α] {f g : → α} (hf : summable (λ (x : ), f x)) (hg : summable (λ (x : ), g x)) :
(∑' (n : ), f n) * ∑' (n : ), g n = ∑' (n : ), (λ (kl : × ), f kl.fst * g kl.snd)

The Cauchy product formula for the product of two infinite sums indexed by ℕ, expressed by summing on finset.nat.antidiagonal. See also tsum_mul_tsum_eq_tsum_sum_antidiagonal if f and g are not absolutely summable.

theorem summable_norm_sum_mul_range_of_summable_norm {α : Type u_1} [normed_ring α] {f g : → α} (hf : summable (λ (x : ), f x)) (hg : summable (λ (x : ), g x)) :
summable (λ (n : ), (finset.range (n + 1)).sum (λ (k : ), f k * g (n - k)))
theorem tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm {α : Type u_1} [normed_ring α] {f g : → α} (hf : summable (λ (x : ), f x)) (hg : summable (λ (x : ), g x)) :
(∑' (n : ), f n) * ∑' (n : ), g n = ∑' (n : ), (finset.range (n + 1)).sum (λ (k : ), f k * g (n - k))

The Cauchy product formula for the product of two infinite sums indexed by ℕ, expressed by summing on finset.range. See also tsum_mul_tsum_eq_tsum_sum_range if f and g are not absolutely summable.

@[class]
structure ring_hom_isometric {R₁ : Type u_5} {R₂ : Type u_6} [semiring R₁] [semiring R₂] [has_norm R₁] [has_norm R₂] (σ : R₁ →+* R₂) :
Prop

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.

Instances of this typeclass
@[protected, instance]
def ring_hom_isometric.ids {R₁ : Type u_5} [semi_normed_ring R₁] :