mathlib3 documentation

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:

Notes #

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

References #

Tags #

ring_seminorm, ring_norm

structure ring_seminorm (R : Type u_4) [non_unital_non_assoc_ring R] :
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
structure ring_norm (R : Type u_4) [non_unital_non_assoc_ring R] :
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
structure mul_ring_seminorm (R : Type u_4) [non_assoc_ring R] :
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
structure mul_ring_norm (R : Type u_4) [non_assoc_ring R] :
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]

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

Equations
@[simp]
@[ext]
theorem ring_seminorm.ext {R : Type u_2} [non_unital_ring R] {p q : ring_seminorm R} :
( (x : R), p x = q x) p = q
@[protected, instance]
Equations
theorem ring_seminorm.eq_zero_iff {R : Type u_2} [non_unital_ring R] {p : ring_seminorm R} :
p = 0 (x : R), p x = 0
theorem ring_seminorm.ne_zero_iff {R : Type u_2} [non_unital_ring R] {p : ring_seminorm R} :
p 0 (x : R), p x 0
@[protected, instance]
Equations
@[protected, instance]

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} [non_unital_ring R] [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
@[protected, instance]

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} [non_unital_ring R] (p : ring_norm R) :
@[ext]
theorem ring_norm.ext {R : Type u_2} [non_unital_ring R] {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) [non_unital_ring R] [decidable_eq R] (x : R) :
1 x = ite (x = 0) 0 1
@[protected, instance]
Equations
@[protected, instance]

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

Equations
@[ext]
theorem mul_ring_seminorm.ext {R : Type u_2} [non_assoc_ring R] {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} [non_assoc_ring R] [decidable_eq R] [no_zero_divisors R] [nontrivial R] (x : R) :
1 x = ite (x = 0) 0 1
@[protected, instance]

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

Equations
@[simp]
@[ext]
theorem mul_ring_norm.ext {R : Type u_2} [non_assoc_ring R] {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) [non_assoc_ring R] [decidable_eq R] [no_zero_divisors R] [nontrivial R] (x : R) :
1 x = ite (x = 0) 0 1
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]

The norm of a normed_ring as a ring_norm.

Equations