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.

Equations
@[simp]
theorem WithTop.coe_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : α) (b : α) :
(a * b) = a * b
theorem WithTop.mul_top' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithTop α) :
a * = if a = 0 then 0 else
@[simp]
theorem WithTop.mul_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithTop α} (h : a 0) :
theorem WithTop.top_mul' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (b : WithTop α) :
* b = if b = 0 then 0 else
@[simp]
theorem WithTop.top_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : WithTop α} (hb : b 0) :
@[simp]
theorem WithTop.top_mul_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] :
theorem WithTop.mul_def {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithTop α) (b : WithTop α) :
a * b = if a = 0 b = 0 then 0 else WithTop.map₂ (fun (x1 x2 : α) => x1 * x2) a b
theorem WithTop.mul_eq_top_iff {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithTop α} {b : WithTop α} :
a * b = a 0 b = a = b 0
theorem WithTop.mul_coe_eq_bind {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : α} (hb : b 0) (a : WithTop α) :
a * b = Option.bind a fun (a : α) => some (a * b)
theorem WithTop.coe_mul_eq_bind {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : α} (ha : a 0) (b : WithTop α) :
a * b = Option.bind b fun (b : α) => some (a * b)
@[simp]
theorem WithTop.untop'_zero_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithTop α) (b : WithTop α) :
theorem WithTop.mul_ne_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithTop α} {b : WithTop α} (ha : a ) (hb : b ) :
a * b
theorem WithTop.mul_lt_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a : WithTop α} {b : WithTop α} (ha : a < ) (hb : b < ) :
a * b <
@[deprecated WithTop.mul_lt_top]
theorem WithTop.mul_lt_top' {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a : WithTop α} {b : WithTop α} (ha : a < ) (hb : b < ) :
a * b <

Alias of WithTop.mul_lt_top.

Equations
  • =

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

Equations
@[simp]
theorem MonoidWithZeroHom.withTopMap_apply {R : Type u_2} {S : Type u_3} [MulZeroOneClass R] [DecidableEq R] [Nontrivial R] [MulZeroOneClass S] [DecidableEq S] [Nontrivial S] (f : R →*₀ S) (hf : Function.Injective f) :
(f.withTopMap hf) = WithTop.map f

A version of WithTop.map for MonoidWithZeroHoms.

Equations
  • f.withTopMap hf = { toFun := WithTop.map f, map_zero' := , map_one' := , map_mul' := }
Instances For
    Equations
    Equations
    @[simp]
    theorem WithTop.coe_pow {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] (a : α) (n : ) :
    (a ^ n) = a ^ n
    theorem WithTop.top_pow {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {n : } (n_pos : 0 < n) :
    Equations

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

    Equations
    Equations
    @[simp]
    theorem RingHom.withTopMap_apply {R : Type u_2} {S : Type u_3} [CanonicallyOrderedCommSemiring R] [DecidableEq R] [Nontrivial R] [CanonicallyOrderedCommSemiring S] [DecidableEq S] [Nontrivial S] (f : R →+* S) (hf : Function.Injective f) :
    (f.withTopMap hf) = (↑(f.toMonoidWithZeroHom.withTopMap hf)).toFun

    A version of WithTop.map for RingHoms.

    Equations
    • f.withTopMap hf = { toFun := (↑(f.toMonoidWithZeroHom.withTopMap hf)).toFun, map_one' := , map_mul' := , map_zero' := , map_add' := }
    Instances For
      Equations
      • WithBot.instMulZeroClass = WithTop.instMulZeroClass
      @[simp]
      theorem WithBot.coe_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : α) (b : α) :
      (a * b) = a * b
      theorem WithBot.mul_bot' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithBot α) :
      a * = if a = 0 then 0 else
      @[simp]
      theorem WithBot.mul_bot {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithBot α} (h : a 0) :
      theorem WithBot.bot_mul' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (b : WithBot α) :
      * b = if b = 0 then 0 else
      @[simp]
      theorem WithBot.bot_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : WithBot α} (hb : b 0) :
      @[simp]
      theorem WithBot.bot_mul_bot {α : Type u_1} [DecidableEq α] [MulZeroClass α] :
      theorem WithBot.mul_def {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithBot α) (b : WithBot α) :
      a * b = if a = 0 b = 0 then 0 else WithBot.map₂ (fun (x1 x2 : α) => x1 * x2) a b
      theorem WithBot.mul_eq_bot_iff {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithBot α} {b : WithBot α} :
      a * b = a 0 b = a = b 0
      theorem WithBot.mul_coe_eq_bind {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : α} (hb : b 0) (a : WithBot α) :
      a * b = Option.bind a fun (a : α) => some (a * b)
      theorem WithBot.coe_mul_eq_bind {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : α} (ha : a 0) (b : WithBot α) :
      a * b = Option.bind b fun (b : α) => some (a * b)
      @[simp]
      theorem WithBot.unbot'_zero_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithBot α) (b : WithBot α) :
      theorem WithBot.mul_ne_bot {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithBot α} {b : WithBot α} (ha : a ) (hb : b ) :
      a * b
      theorem WithBot.bot_lt_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a : WithBot α} {b : WithBot α} (ha : < a) (hb : < b) :
      < a * b
      @[deprecated WithBot.bot_lt_mul]
      theorem WithBot.bot_lt_mul' {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a : WithBot α} {b : WithBot α} (ha : < a) (hb : < b) :
      < a * b

      Alias of WithBot.bot_lt_mul.

      Equations
      • =

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

      Equations
      • WithBot.instMulZeroOneClass = WithTop.instMulZeroOneClass
      Equations
      • WithBot.instSemigroupWithZero = WithTop.instSemigroupWithZero
      Equations
      • WithBot.instMonoidWithZero = WithTop.instMonoidWithZero
      @[simp]
      theorem WithBot.coe_pow {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] (a : α) (n : ) :
      (a ^ n) = a ^ n
      Equations
      • WithBot.commMonoidWithZero = WithTop.instCommMonoidWithZero
      Equations
      • WithBot.commSemiring = WithTop.commSemiring
      Equations
      • =
      Equations
      • =