mathlib3 documentation

algebra.order.ring.with_top

Structures involving * and 0 on with_top and with_bot #

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

The main results of this section are with_top.canonically_ordered_comm_semiring and with_bot.ordered_comm_semiring.

source
@[protected, instance]
def with_top.mul_zero_class {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] :
mul_zero_class (with_top α)
Equations
source
theorem with_top.mul_def {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a b : with_top α} :
a * b = ite (a = 0 ∨ b = 0) 0 (option.map₂ has_mul.mul a b)
source
theorem with_top.mul_top' {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} :
a * ⊤ = ite (a = 0) 0 ⊤
source
@[simp]
theorem with_top.mul_top {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} (h : a ≠ 0) :
a * ⊤ = ⊤
source
theorem with_top.top_mul' {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} :
⊤ * a = ite (a = 0) 0 ⊤
source
@[simp]
theorem with_top.top_mul {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} (h : a ≠ 0) :
⊤ * a = ⊤
source
@[simp]
theorem with_top.top_mul_top {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] :
⊤ * ⊤ = ⊤
source
theorem with_top.mul_eq_top_iff {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a b : with_top α} :
a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
source
theorem with_top.mul_lt_top' {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] [has_lt α] {a b : with_top α} (ha : a < ⊤) (hb : b < ⊤) :
a * b < ⊤
source
theorem with_top.mul_lt_top {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] [has_lt α] {a b : with_top α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
a * b < ⊤
source
@[protected, instance]
def with_top.no_zero_divisors {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] [no_zero_divisors α] :
no_zero_divisors (with_top α)
source
@[simp, norm_cast]
theorem with_top.coe_mul {α : Type u_1} [decidable_eq α] [mul_zero_class α] {a b : α} :
↑(a * b) = ↑a * ↑b
source
theorem with_top.mul_coe {α : Type u_1} [decidable_eq α] [mul_zero_class α] {b : α} (hb : b ≠ 0) {a : with_top α} :
a * ↑b = option.bind a (λ (a : α), ↑(a * b))
source
@[simp]
theorem with_top.untop'_zero_mul {α : Type u_1} [decidable_eq α] [mul_zero_class α] (a b : with_top α) :
with_top.untop' 0 (a * b) = with_top.untop' 0 a * with_top.untop' 0 b
source
@[protected, instance]
def with_top.mul_zero_one_class {α : Type u_1} [decidable_eq α] [mul_zero_one_class α] [nontrivial α] :
mul_zero_one_class (with_top α)

nontrivial α is needed here as otherwise we have 1 * ⊤ = ⊤ but also 0 * ⊤ = 0.

Equations
source
@[simp]
theorem monoid_with_zero_hom.with_top_map_apply {R : Type u_1} {S : Type u_2} [mul_zero_one_class R] [decidable_eq R] [nontrivial R] [mul_zero_one_class S] [decidable_eq S] [nontrivial S] (f : R →*₀ S) (hf : function.injective ⇑f) :
⇑(f.with_top_map hf) = with_top.map ⇑f
source
@[protected]
def monoid_with_zero_hom.with_top_map {R : Type u_1} {S : Type u_2} [mul_zero_one_class R] [decidable_eq R] [nontrivial R] [mul_zero_one_class S] [decidable_eq S] [nontrivial S] (f : R →*₀ S) (hf : function.injective ⇑f) :
with_top R →*₀ with_top S

A version of with_top.map for monoid_with_zero_homs.

Equations
source
@[protected, instance]
def with_top.semigroup_with_zero {α : Type u_1} [decidable_eq α] [semigroup_with_zero α] [no_zero_divisors α] :
semigroup_with_zero (with_top α)
Equations
source
@[protected, instance]
def with_top.monoid_with_zero {α : Type u_1} [decidable_eq α] [monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
monoid_with_zero (with_top α)
Equations
source
@[protected, instance]
def with_top.comm_monoid_with_zero {α : Type u_1} [decidable_eq α] [comm_monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
comm_monoid_with_zero (with_top α)
Equations
source
@[protected, instance]
def with_top.comm_semiring {α : Type u_1} [decidable_eq α] [canonically_ordered_comm_semiring α] [nontrivial α] :
comm_semiring (with_top α)

This instance requires canonically_ordered_comm_semiring as it is the smallest class that derives from both non_assoc_non_unital_semiring and canonically_ordered_add_monoid, both of which are required for distributivity.

Equations
source
@[protected, instance]
def with_top.canonically_ordered_comm_semiring {α : Type u_1} [decidable_eq α] [canonically_ordered_comm_semiring α] [nontrivial α] :
canonically_ordered_comm_semiring (with_top α)
Equations
source
@[protected]
def ring_hom.with_top_map {R : Type u_1} {S : Type u_2} [canonically_ordered_comm_semiring R] [decidable_eq R] [nontrivial R] [canonically_ordered_comm_semiring S] [decidable_eq S] [nontrivial S] (f : R →+* S) (hf : function.injective ⇑f) :
with_top R →+* with_top S

A version of with_top.map for ring_homs.

Equations
source
@[simp]
theorem ring_hom.with_top_map_apply {R : Type u_1} {S : Type u_2} [canonically_ordered_comm_semiring R] [decidable_eq R] [nontrivial R] [canonically_ordered_comm_semiring S] [decidable_eq S] [nontrivial S] (f : R →+* S) (hf : function.injective ⇑f) :
⇑(f.with_top_map hf) = with_top.map ⇑f
source
@[protected, instance]
def with_bot.mul_zero_class {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] :
mul_zero_class (with_bot α)
Equations
source
theorem with_bot.mul_def {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a b : with_bot α} :
a * b = ite (a = 0 ∨ b = 0) 0 (option.map₂ has_mul.mul a b)
source
@[simp]
theorem with_bot.mul_bot {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a : with_bot α} (h : a ≠ 0) :
a * ⊥ = ⊥
source
@[simp]
theorem with_bot.bot_mul {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a : with_bot α} (h : a ≠ 0) :
⊥ * a = ⊥
source
@[simp]
theorem with_bot.bot_mul_bot {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] :
⊥ * ⊥ = ⊥
source
theorem with_bot.mul_eq_bot_iff {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a b : with_bot α} :
a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0
source
theorem with_bot.bot_lt_mul' {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] [has_lt α] {a b : with_bot α} (ha : ⊥ < a) (hb : ⊥ < b) :
⊥ < a * b
source
theorem with_bot.bot_lt_mul {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] [has_lt α] {a b : with_bot α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) :
⊥ < a * b
source
@[norm_cast]
theorem with_bot.coe_mul {α : Type u_1} [decidable_eq α] [mul_zero_class α] {a b : α} :
↑(a * b) = ↑a * ↑b
source
theorem with_bot.mul_coe {α : Type u_1} [decidable_eq α] [mul_zero_class α] {b : α} (hb : b ≠ 0) {a : with_bot α} :
a * ↑b = option.bind a (λ (a : α), ↑(a * b))
source
@[protected, instance]
def with_bot.mul_zero_one_class {α : Type u_1} [decidable_eq α] [mul_zero_one_class α] [nontrivial α] :
mul_zero_one_class (with_bot α)

nontrivial α is needed here as otherwise we have 1 * ⊥ = ⊥ but also = 0 * ⊥ = 0.

Equations
source
@[protected, instance]
def with_bot.no_zero_divisors {α : Type u_1} [decidable_eq α] [mul_zero_class α] [no_zero_divisors α] :
no_zero_divisors (with_bot α)
source
@[protected, instance]
def with_bot.semigroup_with_zero {α : Type u_1} [decidable_eq α] [semigroup_with_zero α] [no_zero_divisors α] :
semigroup_with_zero (with_bot α)
Equations
source
@[protected, instance]
def with_bot.monoid_with_zero {α : Type u_1} [decidable_eq α] [monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
monoid_with_zero (with_bot α)
Equations
source
@[protected, instance]
def with_bot.comm_monoid_with_zero {α : Type u_1} [decidable_eq α] [comm_monoid_with_zero α] [no_zero_divisors α] [nontrivial α] :
comm_monoid_with_zero (with_bot α)
Equations
source
@[protected, instance]
def with_bot.comm_semiring {α : Type u_1} [decidable_eq α] [canonically_ordered_comm_semiring α] [nontrivial α] :
comm_semiring (with_bot α)
Equations
source
@[protected, instance]
def with_bot.pos_mul_mono {α : Type u_1} [decidable_eq α] [mul_zero_class α] [preorder α] [pos_mul_mono α] :
pos_mul_mono (with_bot α)
source
@[protected, instance]
def with_bot.mul_pos_mono {α : Type u_1} [decidable_eq α] [mul_zero_class α] [preorder α] [mul_pos_mono α] :
mul_pos_mono (with_bot α)
source
@[protected, instance]
def with_bot.pos_mul_strict_mono {α : Type u_1} [decidable_eq α] [mul_zero_class α] [preorder α] [pos_mul_strict_mono α] :
pos_mul_strict_mono (with_bot α)
source
@[protected, instance]
def with_bot.mul_pos_strict_mono {α : Type u_1} [decidable_eq α] [mul_zero_class α] [preorder α] [mul_pos_strict_mono α] :
mul_pos_strict_mono (with_bot α)
source
@[protected, instance]
def with_bot.pos_mul_reflect_lt {α : Type u_1} [decidable_eq α] [mul_zero_class α] [preorder α] [pos_mul_reflect_lt α] :
pos_mul_reflect_lt (with_bot α)
source
@[protected, instance]
def with_bot.mul_pos_reflect_lt {α : Type u_1} [decidable_eq α] [mul_zero_class α] [preorder α] [mul_pos_reflect_lt α] :
mul_pos_reflect_lt (with_bot α)
source
@[protected, instance]
def with_bot.pos_mul_mono_rev {α : Type u_1} [decidable_eq α] [mul_zero_class α] [preorder α] [pos_mul_mono_rev α] :
pos_mul_mono_rev (with_bot α)
source
@[protected, instance]
def with_bot.mul_pos_mono_rev {α : Type u_1} [decidable_eq α] [mul_zero_class α] [preorder α] [mul_pos_mono_rev α] :
mul_pos_mono_rev (with_bot α)
source
@[protected, instance]
def with_bot.ordered_comm_semiring {α : Type u_1} [decidable_eq α] [canonically_ordered_comm_semiring α] [nontrivial α] :
ordered_comm_semiring (with_bot α)
Equations