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.

@[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)
theorem with_top.mul_top' {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} :
a * = ite (a = 0) 0
@[simp]
theorem with_top.mul_top {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} (h : a 0) :
theorem with_top.top_mul' {α : Type u_1} [decidable_eq α] [has_zero α] [has_mul α] {a : with_top α} :
* a = ite (a = 0) 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 α] :
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
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 <
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 <
@[protected, instance]
@[simp, 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]
@[protected, instance]

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

Equations
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 α] :
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
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
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
@[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))
@[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]