# mathlib3documentation

analysis.normed.ring.seminorm

# Seminorms and norms on rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines seminorms and norms on rings. These definitions are useful when one needs to consider multiple (semi)norms on a given ring.

## Main declarations #

For a ring R:

• ring_seminorm: A seminorm on a ring R is a function f : R → ℝ that preserves zero, takes nonnegative values, is subadditive and submultiplicative and such that f (-x) = f x for all x ∈ R.
• ring_norm: A seminorm f is a norm if f x = 0 if and only if x = 0.
• mul_ring_seminorm: A multiplicative seminorm on a ring R is a ring seminorm that preserves multiplication.
• mul_ring_norm: A multiplicative norm on a ring R is a ring norm that preserves multiplication.

## Notes #

The corresponding hom classes are defined in analysis.order.hom.basic to be used by absolute values.

## Tags #

ring_seminorm, ring_norm

structure ring_seminorm (R : Type u_4)  :
Type u_4

A seminorm on a ring R is a function f : R → ℝ that preserves zero, takes nonnegative values, is subadditive and submultiplicative and such that f (-x) = f x for all x ∈ R.

Instances for ring_seminorm
@[nolint]
@[nolint]
def ring_norm.to_add_group_norm {R : Type u_4} (self : ring_norm R) :
structure ring_norm (R : Type u_4)  :
Type u_4

A function f : R → ℝ is a norm on a (nonunital) ring if it is a seminorm and f x = 0 implies x = 0.

Instances for ring_norm
@[nolint]
def ring_norm.to_ring_seminorm {R : Type u_4} (self : ring_norm R) :
structure mul_ring_seminorm (R : Type u_4)  :
Type u_4

A multiplicative seminorm on a ring R is a function f : R → ℝ that preserves zero and multiplication, takes nonnegative values, is subadditive and such that f (-x) = f x for all x.

Instances for mul_ring_seminorm
@[nolint]
@[nolint]
def mul_ring_norm.to_add_group_norm {R : Type u_4} (self : mul_ring_norm R) :
structure mul_ring_norm (R : Type u_4)  :
Type u_4

A multiplicative norm on a ring R is a multiplicative ring seminorm such that f x = 0 implies x = 0.

Instances for mul_ring_norm
@[protected, instance]
Equations
@[protected, instance]
def ring_seminorm.has_coe_to_fun {R : Type u_2}  :
(λ (_x : , R )

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations
@[simp]
theorem ring_seminorm.to_fun_eq_coe {R : Type u_2} (p : ring_seminorm R) :
@[ext]
theorem ring_seminorm.ext {R : Type u_2} {p q : ring_seminorm R} :
( (x : R), p x = q x) p = q
@[protected, instance]
def ring_seminorm.has_zero {R : Type u_2}  :
Equations
theorem ring_seminorm.eq_zero_iff {R : Type u_2} {p : ring_seminorm R} :
p = 0 (x : R), p x = 0
theorem ring_seminorm.ne_zero_iff {R : Type u_2} {p : ring_seminorm R} :
p 0 (x : R), p x 0
@[protected, instance]
def ring_seminorm.inhabited {R : Type u_2}  :
Equations
@[protected, instance]
def ring_seminorm.has_one {R : Type u_2} [decidable_eq R] :

The trivial seminorm on a ring R is the ring_seminorm taking value 0 at 0 and 1 at every other element.

Equations
@[simp]
theorem ring_seminorm.apply_one {R : Type u_2} [decidable_eq R] (x : R) :
1 x = ite (x = 0) 0 1
theorem ring_seminorm.seminorm_one_eq_one_iff_ne_zero {R : Type u_2} [ring R] (p : ring_seminorm R) (hp : p 1 1) :
p 1 = 1 p 0
def norm_ring_seminorm (R : Type u_1)  :

The norm of a non_unital_semi_normed_ring as a ring_seminorm.

Equations
@[protected, instance]
def ring_norm.ring_norm_class {R : Type u_2}  :
R
Equations
@[protected, instance]
def ring_norm.has_coe_to_fun {R : Type u_2}  :
(λ (_x : , R )

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations
@[simp]
theorem ring_norm.to_fun_eq_coe {R : Type u_2} (p : ring_norm R) :
@[ext]
theorem ring_norm.ext {R : Type u_2} {p q : ring_norm R} :
( (x : R), p x = q x) p = q
@[protected, instance]

The trivial norm on a ring R is the ring_norm taking value 0 at 0 and 1 at every other element.

Equations
@[simp]
theorem ring_norm.apply_one (R : Type u_2) [decidable_eq R] (x : R) :
1 x = ite (x = 0) 0 1
@[protected, instance]
def ring_norm.inhabited (R : Type u_2) [decidable_eq R] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_ring_seminorm.has_coe_to_fun {R : Type u_2}  :
(λ (_x : , R )

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations
@[simp]
@[ext]
theorem mul_ring_seminorm.ext {R : Type u_2} {p q : mul_ring_seminorm R} :
( (x : R), p x = q x) p = q
@[protected, instance]

The trivial seminorm on a ring R is the mul_ring_seminorm taking value 0 at 0 and 1 at every other element.

Equations
@[simp]
theorem mul_ring_seminorm.apply_one {R : Type u_2} [decidable_eq R] [nontrivial R] (x : R) :
1 x = ite (x = 0) 0 1
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_ring_norm.has_coe_to_fun {R : Type u_2}  :
(λ (_x : , R )

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun.

Equations
@[simp]
theorem mul_ring_norm.to_fun_eq_coe {R : Type u_2} (p : mul_ring_norm R) :
@[ext]
theorem mul_ring_norm.ext {R : Type u_2} {p q : mul_ring_norm R} :
( (x : R), p x = q x) p = q
@[protected, instance]

The trivial norm on a ring R is the mul_ring_norm taking value 0 at 0 and 1 at every other element.

Equations
@[simp]
theorem mul_ring_norm.apply_one (R : Type u_2) [decidable_eq R] [nontrivial R] (x : R) :
1 x = ite (x = 0) 0 1
@[protected, instance]
Equations
def ring_seminorm.to_ring_norm {K : Type u_1} [field K] (f : ring_seminorm K) (hnt : f 0) :

A nonzero ring seminorm on a field K is a ring norm.

Equations
@[simp]
theorem norm_ring_norm_to_fun (R : Type u_1) (ᾰ : R) :
.to_fun =
def norm_ring_norm (R : Type u_1)  :

The norm of a normed_ring as a ring_norm.

Equations