mathlib 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.

@[protected, instance]
def with_top.nontrivial {α : Type u_1} [nonempty α] :
@[protected, instance]
Equations
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)
@[simp]
theorem with_top.mul_top {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} (h : a 0) :
@[simp]
theorem with_top.top_mul {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} (h : a 0) :
@[simp]
theorem with_top.top_mul_top {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] :
@[protected, instance]
@[norm_cast]
theorem with_top.coe_mul {α : Type u_1} [decidable_eq α] [mul_zero_class α] {a b : α} :
(a * b) = a * b
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))
@[simp]
theorem with_top.mul_eq_top_iff {α : Type u_1} [decidable_eq α] [mul_zero_class α] {a b : with_top α} :
a * b = a 0 b = a = b 0
theorem with_top.mul_lt_top {α : Type u_1} [decidable_eq α] [mul_zero_class α] [preorder α] {a b : with_top α} (ha : a ) (hb : b ) :
a * b <
@[simp]
@[protected, instance]

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

Equations
@[protected, instance]
def with_bot.nontrivial {α : Type u_1} [nonempty α] :
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)
@[simp]
theorem with_bot.mul_bot {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a : with_bot α} (h : a 0) :
@[simp]
theorem with_bot.bot_mul {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a : with_bot α} (h : a 0) :
@[simp]
theorem with_bot.bot_mul_bot {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] :
@[norm_cast]
theorem with_bot.coe_mul {α : Type u_1} [decidable_eq α] [mul_zero_class α] {a b : α} :
(a * b) = a * b
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))
@[simp]
theorem with_bot.mul_eq_bot_iff {α : Type u_1} [decidable_eq α] [mul_zero_class α] {a b : with_bot α} :
a * b = a 0 b = a = b 0
theorem with_bot.bot_lt_mul {α : Type u_1} [decidable_eq α] [mul_zero_class α] [preorder α] {a b : with_bot α} (ha : < a) (hb : < b) :
< a * b
@[protected, instance]

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

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]