mathlib documentation

analysis.normed.ring.seminorm

Seminorms and norms on rings #

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:

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
@[class]
structure ring_seminorm_class (F : Type u_4) (α : out_param (Type u_5)) [non_unital_non_assoc_ring α] :
Type (max u_4 u_5)

ring_seminorm_class F α states that F is a type of seminorms on the ring α.

You should extend this class when you extend ring_seminorm.

Instances of this typeclass
Instances of other typeclasses for ring_seminorm_class
  • ring_seminorm_class.has_sizeof_inst
@[class]
structure ring_norm_class (F : Type u_4) (α : out_param (Type u_5)) [non_unital_non_assoc_ring α] :
Type (max u_4 u_5)

ring_norm_class F α states that F is a type of norms on the ring α.

You should extend this class when you extend ring_norm.

Instances of this typeclass
Instances of other typeclasses for ring_norm_class
  • ring_norm_class.has_sizeof_inst
@[class]
structure mul_ring_seminorm_class (F : Type u_4) (α : out_param (Type u_5)) [non_assoc_ring α] :
Type (max u_4 u_5)

mul_ring_seminorm_class F α states that F is a type of multiplicative seminorms on the ring α.

You should extend this class when you extend mul_ring_seminorm.

Instances of this typeclass
Instances of other typeclasses for mul_ring_seminorm_class
  • mul_ring_seminorm_class.has_sizeof_inst
@[class]
structure mul_ring_norm_class (F : Type u_4) (α : out_param (Type u_5)) [non_assoc_ring α] :
Type (max u_4 u_5)

mul_ring_norm_class F α states that F is a type of multiplicative norms on the ring α.

You should extend this class when you extend mul_ring_norm.

Instances of this typeclass
Instances of other typeclasses for mul_ring_norm_class
  • mul_ring_norm_class.has_sizeof_inst
@[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