Documentation

Mathlib.Algebra.Order.Ring.WithTop

Structures involving * and 0 on WithTop and WithBot #

The main results of this section are WithTop.canonicallyOrderedCommSemiring and WithBot.orderedCommSemiring.

theorem WithTop.mul_def {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] {a : WithTop α} {b : WithTop α} :
a * b = if a = 0 b = 0 then 0 else Option.map₂ (fun x x_1 => x * x_1) a b
theorem WithTop.top_mul_top {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] :
theorem WithTop.mul_top' {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] (a : WithTop α) :
a * = if a = 0 then 0 else
@[simp]
theorem WithTop.mul_top {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] {a : WithTop α} (h : a 0) :
theorem WithTop.top_mul' {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] (a : WithTop α) :
* a = if a = 0 then 0 else
@[simp]
theorem WithTop.top_mul {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] {a : WithTop α} (h : a 0) :
theorem WithTop.mul_eq_top_iff {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] {a : WithTop α} {b : WithTop α} :
a * b = a 0 b = a = b 0
theorem WithTop.mul_lt_top' {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] [LT α] {a : WithTop α} {b : WithTop α} (ha : a < ) (hb : b < ) :
a * b <
theorem WithTop.mul_lt_top {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] [LT α] {a : WithTop α} {b : WithTop α} (ha : a ) (hb : b ) :
a * b <
@[simp]
theorem WithTop.coe_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : α} {b : α} :
↑(a * b) = a * b
theorem WithTop.mul_coe {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : α} (hb : b 0) {a : WithTop α} :
a * b = Option.bind a fun a => some (a * b)
@[simp]
theorem WithTop.untop'_zero_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithTop α) (b : WithTop α) :

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

This instance requires CanonicallyOrderedCommSemiring as it is the smallest class that derives from both NonAssocNonUnitalSemiring and CanonicallyOrderedAddMonoid, both of which are required for distributivity.

theorem WithBot.mul_def {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] {a : WithBot α} {b : WithBot α} :
a * b = if a = 0 b = 0 then 0 else Option.map₂ (fun x x_1 => x * x_1) a b
@[simp]
theorem WithBot.mul_bot {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] {a : WithBot α} (h : a 0) :
@[simp]
theorem WithBot.bot_mul {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] {a : WithBot α} (h : a 0) :
@[simp]
theorem WithBot.bot_mul_bot {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] :
theorem WithBot.mul_eq_bot_iff {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] {a : WithBot α} {b : WithBot α} :
a * b = a 0 b = a = b 0
theorem WithBot.bot_lt_mul' {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] [LT α] {a : WithBot α} {b : WithBot α} (ha : < a) (hb : < b) :
< a * b
theorem WithBot.bot_lt_mul {α : Type u_1} [DecidableEq α] [Zero α] [Mul α] [LT α] {a : WithBot α} {b : WithBot α} (ha : a ) (hb : b ) :
< a * b
@[simp]
theorem WithBot.coe_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : α} {b : α} :
↑(a * b) = a * b
theorem WithBot.mul_coe {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : α} (hb : b 0) {a : WithBot α} :
a * b = Option.bind a fun a => some (a * b)

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