mathlib3 documentation

algebra.order.hom.basic

Algebraic order homomorphism classes #

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

This file defines hom classes for common properties at the intersection of order theory and algebra.

Typeclasses #

Basic typeclasses

nonneg_hom_class: Homs are nonnegative: ∀ f a, 0 ≤ f a
subadditive_hom_class: Homs are subadditive: ∀ f a b, f (a + b) ≤ f a + f b
submultiplicative_hom_class: Homs are submultiplicative: ∀ f a b, f (a * b) ≤ f a * f b
mul_le_add_hom_class: ∀ f a b, f (a * b) ≤ f a + f b
nonarchimedean_hom_class: ∀ a b, f (a + b) ≤ max (f a) (f b)

Group norms

add_group_seminorm_class: Homs are nonnegative, subadditive, even and preserve zero.
group_seminorm_class: Homs are nonnegative, respect f (a * b) ≤ f a + f b, f a⁻¹ = f a and preserve zero.
add_group_norm_class: Homs are seminorms such that f x = 0 → x = 0 for all x.
group_norm_class: Homs are seminorms such that f x = 0 → x = 1 for all x.

Ring norms

ring_seminorm_class: Homs are submultiplicative group norms.
ring_norm_class: Homs are ring seminorms that are also additive group norms.
mul_ring_seminorm_class: Homs are ring seminorms that are multiplicative.
mul_ring_norm_class: Homs are ring norms that are multiplicative.

Notes #

Typeclasses for seminorms are defined here while types of seminorms are defined in analysis.normed.group.seminorm and analysis.normed.ring.seminorm because absolute values are multiplicative ring norms but outside of this use we only consider real-valued seminorms.

TODO #

Finitary versions of the current lemmas.

def library_note.out-param inheritance :

Diamond inheritance cannot depend on out_params in the following circumstances:

there are three classes top, middle, bottom
all of these classes have a parameter (α : out_param _)
all of these classes have an instance parameter [root α] that depends on this out_param
the root class has two child classes: left and right, these are siblings in the hierarchy
the instance bottom.to_middle takes a [left α] parameter
the instance middle.to_top takes a [right α] parameter
there is a leaf class that inherits from both left and right. In that case, given instances bottom α and leaf α, Lean cannot synthesize a top α instance, even though the hypotheses of the instances bottom.to_middle and middle.to_top are satisfied.

There are two workarounds:

You could replace the bundled inheritance implemented by the instance middle.to_top with unbundled inheritance implemented by adding a [top α] parameter to the middle class. This is the preferred option since it is also more compatible with Lean 4, at the cost of being more work to implement and more verbose to use.
You could weaken the bottom.to_middle instance by making it depend on a subclass of middle.to_top's parameter, in this example replacing [left α] with [leaf α].

Basics #

@[class]

structure nonneg_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_zero β] [has_le β] :

Type (max u_7 u_8 u_9)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective nonneg_hom_class.coe
map_nonneg : ∀ (f : F) (a : α), 0 ≤ ⇑f a

nonneg_hom_class F α β states that F is a type of nonnegative morphisms.

Instances of this typeclass

Instances of other typeclasses for nonneg_hom_class

nonneg_hom_class.has_sizeof_inst

@[instance]

def nonneg_hom_class.to_fun_like (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_zero β] [has_le β] [self : nonneg_hom_class F α β] :

fun_like F α (λ (_x : α), β)

@[instance]

def subadditive_hom_class.to_fun_like (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_add α] [has_add β] [has_le β] [self : subadditive_hom_class F α β] :

fun_like F α (λ (_x : α), β)

@[class]

structure subadditive_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_add α] [has_add β] [has_le β] :

Type (max u_7 u_8 u_9)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective subadditive_hom_class.coe
map_add_le_add : ∀ (f : F) (a b : α), ⇑f (a + b) ≤ ⇑f a + ⇑f b

subadditive_hom_class F α β states that F is a type of subadditive morphisms.

Instances of this typeclass

Instances of other typeclasses for subadditive_hom_class

subadditive_hom_class.has_sizeof_inst

@[instance]

def submultiplicative_hom_class.to_fun_like (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_mul α] [has_mul β] [has_le β] [self : submultiplicative_hom_class F α β] :

fun_like F α (λ (_x : α), β)

@[class]

structure submultiplicative_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_mul α] [has_mul β] [has_le β] :

Type (max u_7 u_8 u_9)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective submultiplicative_hom_class.coe
map_mul_le_mul : ∀ (f : F) (a b : α), ⇑f (a * b) ≤ ⇑f a * ⇑f b

submultiplicative_hom_class F α β states that F is a type of submultiplicative morphisms.

Instances of this typeclass

ring_seminorm_class.to_submultiplicative_hom_class

Instances of other typeclasses for submultiplicative_hom_class

submultiplicative_hom_class.has_sizeof_inst

@[class]

structure mul_le_add_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_mul α] [has_add β] [has_le β] :

Type (max u_7 u_8 u_9)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective mul_le_add_hom_class.coe
map_mul_le_add : ∀ (f : F) (a b : α), ⇑f (a * b) ≤ ⇑f a + ⇑f b

mul_le_add_hom_class F α β states that F is a type of subadditive morphisms.

Instances of this typeclass

group_seminorm_class.to_mul_le_add_hom_class

Instances of other typeclasses for mul_le_add_hom_class

mul_le_add_hom_class.has_sizeof_inst

@[instance]

def mul_le_add_hom_class.to_fun_like (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_mul α] [has_add β] [has_le β] [self : mul_le_add_hom_class F α β] :

fun_like F α (λ (_x : α), β)

@[class]

structure nonarchimedean_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_add α] [linear_order β] :

Type (max u_7 u_8 u_9)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective nonarchimedean_hom_class.coe
map_add_le_max : ∀ (f : F) (a b : α), ⇑f (a + b) ≤ linear_order.max (⇑f a) (⇑f b)

nonarchimedean_hom_class F α β states that F is a type of non-archimedean morphisms.

Instances of this typeclass

nonarch_add_group_seminorm_class.to_nonarchimedean_hom_class

Instances of other typeclasses for nonarchimedean_hom_class

nonarchimedean_hom_class.has_sizeof_inst

@[instance]

def nonarchimedean_hom_class.to_fun_like (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [has_add α] [linear_order β] [self : nonarchimedean_hom_class F α β] :

fun_like F α (λ (_x : α), β)

theorem le_map_add_map_sub {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [add_comm_semigroup β] [has_le β] [subadditive_hom_class F α β] (f : F) (a b : α) :

⇑f a ≤ ⇑f b + ⇑f (a - b)

theorem le_map_mul_map_div {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [comm_semigroup β] [has_le β] [submultiplicative_hom_class F α β] (f : F) (a b : α) :

⇑f a ≤ ⇑f b * ⇑f (a / b)

theorem le_map_add_map_div {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [add_comm_semigroup β] [has_le β] [mul_le_add_hom_class F α β] (f : F) (a b : α) :

⇑f a ≤ ⇑f b + ⇑f (a / b)

theorem le_map_div_mul_map_div {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [comm_semigroup β] [has_le β] [submultiplicative_hom_class F α β] (f : F) (a b c : α) :

⇑f (a / c) ≤ ⇑f (a / b) * ⇑f (b / c)

theorem le_map_sub_add_map_sub {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [add_comm_semigroup β] [has_le β] [subadditive_hom_class F α β] (f : F) (a b c : α) :

⇑f (a - c) ≤ ⇑f (a - b) + ⇑f (b - c)

theorem le_map_div_add_map_div {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [add_comm_semigroup β] [has_le β] [mul_le_add_hom_class F α β] (f : F) (a b c : α) :

⇑f (a / c) ≤ ⇑f (a / b) + ⇑f (b / c)

Group (semi)norms #

@[class]

structure add_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [add_group α] [ordered_add_comm_monoid β] :

Type (max u_7 u_8 u_9)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective add_group_seminorm_class.coe
map_add_le_add : ∀ (f : F) (a b : α), ⇑f (a + b) ≤ ⇑f a + ⇑f b
map_zero : ∀ (f : F), ⇑f 0 = 0
map_neg_eq_map : ∀ (f : F) (a : α), ⇑f (-a) = ⇑f a

add_group_seminorm_class F α states that F is a type of β-valued seminorms on the additive group α.

You should extend this class when you extend add_group_seminorm.

Instances of this typeclass

Instances of other typeclasses for add_group_seminorm_class

add_group_seminorm_class.has_sizeof_inst

@[instance]

def add_group_seminorm_class.to_subadditive_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [add_group α] [ordered_add_comm_monoid β] [self : add_group_seminorm_class F α β] :

subadditive_hom_class F α β

@[instance]

def group_seminorm_class.to_mul_le_add_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [group α] [ordered_add_comm_monoid β] [self : group_seminorm_class F α β] :

mul_le_add_hom_class F α β

@[class]

structure group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [group α] [ordered_add_comm_monoid β] :

Type (max u_7 u_8 u_9)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective group_seminorm_class.coe
map_mul_le_add : ∀ (f : F) (a b : α), ⇑f (a * b) ≤ ⇑f a + ⇑f b
map_one_eq_zero : ∀ (f : F), ⇑f 1 = 0
map_inv_eq_map : ∀ (f : F) (a : α), ⇑f a⁻¹ = ⇑f a

group_seminorm_class F α states that F is a type of β-valued seminorms on the group α.

You should extend this class when you extend group_seminorm.

Instances of this typeclass

Instances of other typeclasses for group_seminorm_class

group_seminorm_class.has_sizeof_inst

@[instance]

def add_group_norm_class.to_add_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [add_group α] [ordered_add_comm_monoid β] [self : add_group_norm_class F α β] :

add_group_seminorm_class F α β

@[class]

structure add_group_norm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [add_group α] [ordered_add_comm_monoid β] :

Type (max u_7 u_8 u_9)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective add_group_norm_class.coe
map_add_le_add : ∀ (f : F) (a b : α), ⇑f (a + b) ≤ ⇑f a + ⇑f b
map_zero : ∀ (f : F), ⇑f 0 = 0
map_neg_eq_map : ∀ (f : F) (a : α), ⇑f (-a) = ⇑f a
eq_zero_of_map_eq_zero : ∀ (f : F) {a : α}, ⇑f a = 0 → a = 0

add_group_norm_class F α states that F is a type of β-valued norms on the additive group α.

You should extend this class when you extend add_group_norm.

Instances of this typeclass

Instances of other typeclasses for add_group_norm_class

add_group_norm_class.has_sizeof_inst

@[class]

structure group_norm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [group α] [ordered_add_comm_monoid β] :

Type (max u_7 u_8 u_9)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective group_norm_class.coe
map_mul_le_add : ∀ (f : F) (a b : α), ⇑f (a * b) ≤ ⇑f a + ⇑f b
map_one_eq_zero : ∀ (f : F), ⇑f 1 = 0
map_inv_eq_map : ∀ (f : F) (a : α), ⇑f a⁻¹ = ⇑f a
eq_one_of_map_eq_zero : ∀ (f : F) {a : α}, ⇑f a = 0 → a = 1

group_norm_class F α states that F is a type of β-valued norms on the group α.

You should extend this class when you extend group_norm.

Instances of this typeclass

group_norm.group_norm_class

Instances of other typeclasses for group_norm_class

group_norm_class.has_sizeof_inst

@[instance]

def group_norm_class.to_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [group α] [ordered_add_comm_monoid β] [self : group_norm_class F α β] :

group_seminorm_class F α β

@[instance]

def add_group_seminorm_class.to_add_le_add_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [add_group α] [ordered_add_comm_monoid β] [self : add_group_seminorm_class F α β] :

subadditive_hom_class F α β

@[protected, instance]

def add_group_seminorm_class.to_zero_hom_class {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ordered_add_comm_monoid β] [add_group_seminorm_class F α β] :

zero_hom_class F α β

Equations

add_group_seminorm_class.to_zero_hom_class = {coe := add_group_seminorm_class.coe _inst_3, coe_injective' := _, map_zero := _}

theorem map_div_le_add {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [ordered_add_comm_monoid β] [group_seminorm_class F α β] (f : F) (x y : α) :

⇑f (x / y) ≤ ⇑f x + ⇑f y

theorem map_sub_le_add {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ordered_add_comm_monoid β] [add_group_seminorm_class F α β] (f : F) (x y : α) :

⇑f (x - y) ≤ ⇑f x + ⇑f y

theorem map_sub_rev {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ordered_add_comm_monoid β] [add_group_seminorm_class F α β] (f : F) (x y : α) :

⇑f (x - y) = ⇑f (y - x)

theorem map_div_rev {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [ordered_add_comm_monoid β] [group_seminorm_class F α β] (f : F) (x y : α) :

⇑f (x / y) = ⇑f (y / x)

theorem le_map_add_map_sub' {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ordered_add_comm_monoid β] [add_group_seminorm_class F α β] (f : F) (x y : α) :

⇑f x ≤ ⇑f y + ⇑f (y - x)

theorem le_map_add_map_div' {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [ordered_add_comm_monoid β] [group_seminorm_class F α β] (f : F) (x y : α) :

⇑f x ≤ ⇑f y + ⇑f (y / x)

theorem abs_sub_map_le_div {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [linear_ordered_add_comm_group β] [group_seminorm_class F α β] (f : F) (x y : α) :

|⇑f x - ⇑f y| ≤ ⇑f (x / y)

theorem abs_sub_map_le_sub {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [linear_ordered_add_comm_group β] [add_group_seminorm_class F α β] (f : F) (x y : α) :

|⇑f x - ⇑f y| ≤ ⇑f (x - y)

@[protected, instance]

def add_group_seminorm_class.to_nonneg_hom_class {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [linear_ordered_add_comm_monoid β] [add_group_seminorm_class F α β] :

nonneg_hom_class F α β

Equations

add_group_seminorm_class.to_nonneg_hom_class = {coe := add_group_seminorm_class.coe _inst_3, coe_injective' := _, map_nonneg := _}

@[protected, instance]

def group_seminorm_class.to_nonneg_hom_class {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [linear_ordered_add_comm_monoid β] [group_seminorm_class F α β] :

nonneg_hom_class F α β

Equations

group_seminorm_class.to_nonneg_hom_class = {coe := group_seminorm_class.coe _inst_3, coe_injective' := _, map_nonneg := _}

@[simp]

theorem map_eq_zero_iff_eq_one {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [ordered_add_comm_monoid β] [group_norm_class F α β] (f : F) {x : α} :

⇑f x = 0 ↔ x = 1

@[simp]

theorem map_eq_zero_iff_eq_zero {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ordered_add_comm_monoid β] [add_group_norm_class F α β] (f : F) {x : α} :

⇑f x = 0 ↔ x = 0

theorem map_ne_zero_iff_ne_one {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [ordered_add_comm_monoid β] [group_norm_class F α β] (f : F) {x : α} :

⇑f x ≠ 0 ↔ x ≠ 1

theorem map_ne_zero_iff_ne_zero {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [ordered_add_comm_monoid β] [add_group_norm_class F α β] (f : F) {x : α} :

⇑f x ≠ 0 ↔ x ≠ 0

theorem map_pos_of_ne_zero {F : Type u_2} {α : Type u_3} {β : Type u_4} [add_group α] [linear_ordered_add_comm_monoid β] [add_group_norm_class F α β] (f : F) {x : α} (hx : x ≠ 0) :

0 < ⇑f x

theorem map_pos_of_ne_one {F : Type u_2} {α : Type u_3} {β : Type u_4} [group α] [linear_ordered_add_comm_monoid β] [group_norm_class F α β] (f : F) {x : α} (hx : x ≠ 1) :

0 < ⇑f x

Ring (semi)norms #

@[instance]

def ring_seminorm_class.to_submultiplicative_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [non_unital_non_assoc_ring α] [ordered_semiring β] [self : ring_seminorm_class F α β] :

submultiplicative_hom_class F α β

@[class]

structure ring_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [non_unital_non_assoc_ring α] [ordered_semiring β] :

Type (max u_7 u_8 u_9)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective ring_seminorm_class.coe
map_add_le_add : ∀ (f : F) (a b : α), ⇑f (a + b) ≤ ⇑f a + ⇑f b
map_zero : ∀ (f : F), ⇑f 0 = 0
map_neg_eq_map : ∀ (f : F) (a : α), ⇑f (-a) = ⇑f a
map_mul_le_mul : ∀ (f : F) (a b : α), ⇑f (a * b) ≤ ⇑f a * ⇑f b

ring_seminorm_class F α states that F is a type of β-valued 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

@[instance]

def ring_seminorm_class.to_add_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [non_unital_non_assoc_ring α] [ordered_semiring β] [self : ring_seminorm_class F α β] :

add_group_seminorm_class F α β

@[instance]

def ring_norm_class.to_add_group_norm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [non_unital_non_assoc_ring α] [ordered_semiring β] [self : ring_norm_class F α β] :

add_group_norm_class F α β

@[instance]

def ring_norm_class.to_ring_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [non_unital_non_assoc_ring α] [ordered_semiring β] [self : ring_norm_class F α β] :

ring_seminorm_class F α β

@[class]

structure ring_norm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [non_unital_non_assoc_ring α] [ordered_semiring β] :

Type (max u_7 u_8 u_9)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective ring_norm_class.coe
map_add_le_add : ∀ (f : F) (a b : α), ⇑f (a + b) ≤ ⇑f a + ⇑f b
map_zero : ∀ (f : F), ⇑f 0 = 0
map_neg_eq_map : ∀ (f : F) (a : α), ⇑f (-a) = ⇑f a
map_mul_le_mul : ∀ (f : F) (a b : α), ⇑f (a * b) ≤ ⇑f a * ⇑f b
eq_zero_of_map_eq_zero : ∀ (f : F) {a : α}, ⇑f a = 0 → a = 0

ring_norm_class F α states that F is a type of β-valued 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

@[instance]

def mul_ring_seminorm_class.to_add_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [non_assoc_ring α] [ordered_semiring β] [self : mul_ring_seminorm_class F α β] :

add_group_seminorm_class F α β

@[class]

structure mul_ring_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [non_assoc_ring α] [ordered_semiring β] :

Type (max u_7 u_8 u_9)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective mul_ring_seminorm_class.coe
map_add_le_add : ∀ (f : F) (a b : α), ⇑f (a + b) ≤ ⇑f a + ⇑f b
map_zero : ∀ (f : F), ⇑f 0 = 0
map_neg_eq_map : ∀ (f : F) (a : α), ⇑f (-a) = ⇑f a
map_mul : ∀ (f : F) (x y : α), ⇑f (x * y) = ⇑f x * ⇑f y
map_one : ∀ (f : F), ⇑f 1 = 1

mul_ring_seminorm_class F α states that F is a type of β-valued 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

@[instance]

def mul_ring_seminorm_class.to_monoid_with_zero_hom_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [non_assoc_ring α] [ordered_semiring β] [self : mul_ring_seminorm_class F α β] :

monoid_with_zero_hom_class F α β

@[instance]

def mul_ring_norm_class.to_mul_ring_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [non_assoc_ring α] [ordered_semiring β] [self : mul_ring_norm_class F α β] :

mul_ring_seminorm_class F α β

@[instance]

def mul_ring_norm_class.to_add_group_norm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [non_assoc_ring α] [ordered_semiring β] [self : mul_ring_norm_class F α β] :

add_group_norm_class F α β

@[class]

structure mul_ring_norm_class (F : Type u_7) (α : out_param (Type u_8)) (β : out_param (Type u_9)) [non_assoc_ring α] [ordered_semiring β] :

Type (max u_7 u_8 u_9)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective mul_ring_norm_class.coe
map_add_le_add : ∀ (f : F) (a b : α), ⇑f (a + b) ≤ ⇑f a + ⇑f b
map_zero : ∀ (f : F), ⇑f 0 = 0
map_neg_eq_map : ∀ (f : F) (a : α), ⇑f (-a) = ⇑f a
map_mul : ∀ (f : F) (x y : α), ⇑f (x * y) = ⇑f x * ⇑f y
map_one : ∀ (f : F), ⇑f 1 = 1
eq_zero_of_map_eq_zero : ∀ (f : F) {a : α}, ⇑f a = 0 → a = 0

mul_ring_norm_class F α states that F is a type of β-valued 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]

def ring_seminorm_class.to_nonneg_hom_class {F : Type u_2} {α : Type u_3} {β : Type u_4} [non_unital_non_assoc_ring α] [linear_ordered_semiring β] [ring_seminorm_class F α β] :

nonneg_hom_class F α β

Equations

ring_seminorm_class.to_nonneg_hom_class = add_group_seminorm_class.to_nonneg_hom_class

@[protected, instance]

def mul_ring_seminorm_class.to_ring_seminorm_class {F : Type u_2} {α : Type u_3} {β : Type u_4} [non_assoc_ring α] [ordered_semiring β] [mul_ring_seminorm_class F α β] :

ring_seminorm_class F α β

Equations

mul_ring_seminorm_class.to_ring_seminorm_class = {coe := mul_ring_seminorm_class.coe _inst_3, coe_injective' := _, map_add_le_add := _, map_zero := _, map_neg_eq_map := _, map_mul_le_mul := _}

@[protected, instance]

def mul_ring_norm_class.to_ring_norm_class {F : Type u_2} {α : Type u_3} {β : Type u_4} [non_assoc_ring α] [ordered_semiring β] [mul_ring_norm_class F α β] :

ring_norm_class F α β

Equations

mul_ring_norm_class.to_ring_norm_class = {coe := mul_ring_norm_class.coe _inst_3, coe_injective' := _, map_add_le_add := _, map_zero := _, map_neg_eq_map := _, map_mul_le_mul := _, eq_zero_of_map_eq_zero := _}