Documentation

Mathlib.Algebra.Order.Ring.WithTop

Structures involving * and 0 on WithTop and WithBot #

The main results of this section are WithTop.instOrderedCommSemiring and WithBot.instOrderedCommSemiring.

source
instance WithTop.instMulZeroClass {α : Type u_1} [DecidableEq α] [MulZeroClass α] :
MulZeroClass (WithTop α)
Equations
    source
    @[simp]
    theorem WithTop.coe_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a b : α) :
    ↑(a * b) = ↑a * ↑b
    source
    theorem WithTop.mul_top' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithTop α) :
    a * ⊤ = if a = 0 then 0 else ⊤
    source
    @[simp]
    theorem WithTop.mul_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithTop α} (h : a ≠ 0) :
    a * ⊤ = ⊤
    source
    theorem WithTop.top_mul' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (b : WithTop α) :
    ⊤ * b = if b = 0 then 0 else ⊤
    source
    @[simp]
    theorem WithTop.top_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : WithTop α} (hb : b ≠ 0) :
    ⊤ * b = ⊤
    source
    @[simp]
    theorem WithTop.top_mul_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] :
    ⊤ * ⊤ = ⊤
    source
    theorem WithTop.mul_def {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a b : WithTop α) :
    a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) => x1 * x2) a b
    source
    theorem WithTop.mul_eq_top_iff {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a b : WithTop α} :
    a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
    source
    theorem WithTop.mul_coe_eq_bind {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : α} (hb : b ≠ 0) (a : WithTop α) :
    a * ↑b = Option.bind a fun (a : α) => Option.some (a * b)
    source
    theorem WithTop.coe_mul_eq_bind {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : α} (ha : a ≠ 0) (b : WithTop α) :
    ↑a * b = Option.bind b fun (b : α) => Option.some (a * b)
    source
    @[simp]
    theorem WithTop.untopD_zero_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a b : WithTop α) :
    untopD 0 (a * b) = untopD 0 a * untopD 0 b
    source
    @[deprecated WithTop.untopD_zero_mul (since := "2025-02-06")]
    theorem WithTop.untop'_zero_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a b : WithTop α) :
    untopD 0 (a * b) = untopD 0 a * untopD 0 b

    Alias of WithTop.untopD_zero_mul.

    source
    theorem WithTop.mul_ne_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
    a * b ≠ ⊤
    source
    theorem WithTop.mul_lt_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a b : WithTop α} (ha : a < ⊤) (hb : b < ⊤) :
    a * b < ⊤
    source
    instance WithTop.instNoZeroDivisors {α : Type u_1} [DecidableEq α] [MulZeroClass α] [NoZeroDivisors α] :
    NoZeroDivisors (WithTop α)
    source
    instance WithTop.instMulZeroOneClass {α : Type u_1} [DecidableEq α] [MulZeroOneClass α] [Nontrivial α] :
    MulZeroOneClass (WithTop α)

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

    Equations
      source
      def MonoidWithZeroHom.withTopMap {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) :
      WithTop R →*₀ WithTop S

      A version of WithTop.map for MonoidWithZeroHoms.

      Equations
        Instances For
          source
          @[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
          source
          instance WithTop.instSemigroupWithZero {α : Type u_1} [DecidableEq α] [SemigroupWithZero α] [NoZeroDivisors α] :
          SemigroupWithZero (WithTop α)
          Equations
            source
            instance WithTop.instMonoidWithZero {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] :
            MonoidWithZero (WithTop α)
            Equations
              source
              @[simp]
              theorem WithTop.coe_pow {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] (a : α) (n : ℕ) :
              ↑(a ^ n) = ↑a ^ n
              source
              @[simp]
              theorem WithTop.top_pow {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {n : ℕ} :
              n ≠ 0 → ⊤ ^ n = ⊤
              source
              @[simp]
              theorem WithTop.pow_eq_top_iff {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithTop α} {n : ℕ} :
              x ^ n = ⊤ ↔ x = ⊤ ∧ n ≠ 0
              source
              theorem WithTop.pow_ne_top_iff {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithTop α} {n : ℕ} :
              x ^ n ≠ ⊤ ↔ x ≠ ⊤ ∨ n = 0
              source
              @[simp]
              theorem WithTop.pow_lt_top_iff {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithTop α} {n : ℕ} [Preorder α] :
              x ^ n < ⊤ ↔ x < ⊤ ∨ n = 0
              source
              theorem WithTop.eq_top_of_pow {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithTop α} (n : ℕ) (hx : x ^ n = ⊤) :
              x = ⊤
              source
              theorem WithTop.pow_ne_top {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithTop α} {n : ℕ} (hx : x ≠ ⊤) :
              x ^ n ≠ ⊤
              source
              theorem WithTop.pow_lt_top {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {x : WithTop α} {n : ℕ} [Preorder α] (hx : x < ⊤) :
              x ^ n < ⊤
              source
              instance WithTop.instCommMonoidWithZero {α : Type u_1} [DecidableEq α] [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] :
              CommMonoidWithZero (WithTop α)
              Equations
                source
                instance WithTop.instNonUnitalNonAssocSemiring {α : Type u_1} [DecidableEq α] [NonUnitalNonAssocSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] :
                NonUnitalNonAssocSemiring (WithTop α)
                Equations
                  source
                  instance WithTop.instNonAssocSemiring {α : Type u_1} [DecidableEq α] [NonAssocSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [Nontrivial α] :
                  NonAssocSemiring (WithTop α)
                  Equations
                    source
                    instance WithTop.instNonUnitalSemiring {α : Type u_1} [DecidableEq α] [NonUnitalSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] :
                    NonUnitalSemiring (WithTop α)
                    Equations
                      source
                      instance WithTop.instSemiring {α : Type u_1} [DecidableEq α] [Semiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] :
                      Semiring (WithTop α)
                      Equations
                        source
                        instance WithTop.instCommSemiring {α : Type u_1} [DecidableEq α] [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] :
                        CommSemiring (WithTop α)
                        Equations
                          source
                          instance WithTop.instIsOrderedRing {α : Type u_1} [DecidableEq α] [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] :
                          IsOrderedRing (WithTop α)
                          source
                          def RingHom.withTopMap {R : Type u_2} {S : Type u_3} [NonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [DecidableEq R] [Nontrivial R] [NonAssocSemiring S] [PartialOrder S] [CanonicallyOrderedAdd S] [DecidableEq S] [Nontrivial S] (f : R →+* S) (hf : Function.Injective ⇑f) :
                          WithTop R →+* WithTop S

                          A version of WithTop.map for RingHoms.

                          Equations
                            Instances For
                              source
                              @[simp]
                              theorem RingHom.withTopMap_apply {R : Type u_2} {S : Type u_3} [NonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [DecidableEq R] [Nontrivial R] [NonAssocSemiring S] [PartialOrder S] [CanonicallyOrderedAdd S] [DecidableEq S] [Nontrivial S] (f : R →+* S) (hf : Function.Injective ⇑f) :
                              ⇑(f.withTopMap hf) = (↑(f.toMonoidWithZeroHom.withTopMap hf)).toFun
                              source
                              theorem WithTop.mul_lt_mul {α : Type u_1} [DecidableEq α] [CommSemiring α] [PartialOrder α] [OrderBot α] [CanonicallyOrderedAdd α] [PosMulStrictMono α] {a₁ a₂ b₁ b₂ : WithTop α} (ha : a₁ < a₂) (hb : b₁ < b₂) :
                              a₁ * b₁ < a₂ * b₂
                              source
                              theorem WithTop.pow_right_strictMono {α : Type u_1} [DecidableEq α] [CommSemiring α] [PartialOrder α] [OrderBot α] [CanonicallyOrderedAdd α] [PosMulStrictMono α] [NoZeroDivisors α] [Nontrivial α] {n : ℕ} :
                              n ≠ 0 → StrictMono fun (a : WithTop α) => a ^ n
                              source
                              theorem WithTop.pow_lt_pow_left {α : Type u_1} [DecidableEq α] [CommSemiring α] [PartialOrder α] [OrderBot α] [CanonicallyOrderedAdd α] [PosMulStrictMono α] [NoZeroDivisors α] [Nontrivial α] {a b : WithTop α} (hab : a < b) {n : ℕ} (hn : n ≠ 0) :
                              a ^ n < b ^ n
                              source
                              instance WithBot.instMulZeroClass {α : Type u_1} [DecidableEq α] [MulZeroClass α] :
                              MulZeroClass (WithBot α)
                              Equations
                                source
                                @[simp]
                                theorem WithBot.coe_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a b : α) :
                                ↑(a * b) = ↑a * ↑b
                                source
                                theorem WithBot.mul_bot' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithBot α) :
                                a * ⊥ = if a = 0 then 0 else ⊥
                                source
                                @[simp]
                                theorem WithBot.mul_bot {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithBot α} (h : a ≠ 0) :
                                a * ⊥ = ⊥
                                source
                                theorem WithBot.bot_mul' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (b : WithBot α) :
                                ⊥ * b = if b = 0 then 0 else ⊥
                                source
                                @[simp]
                                theorem WithBot.bot_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : WithBot α} (hb : b ≠ 0) :
                                ⊥ * b = ⊥
                                source
                                @[simp]
                                theorem WithBot.bot_mul_bot {α : Type u_1} [DecidableEq α] [MulZeroClass α] :
                                ⊥ * ⊥ = ⊥
                                source
                                theorem WithBot.mul_def {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a b : WithBot α) :
                                a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun (x1 x2 : α) => x1 * x2) a b
                                source
                                theorem WithBot.mul_eq_bot_iff {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a b : WithBot α} :
                                a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0
                                source
                                theorem WithBot.mul_coe_eq_bind {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : α} (hb : b ≠ 0) (a : WithBot α) :
                                a * ↑b = Option.bind a fun (a : α) => Option.some (a * b)
                                source
                                theorem WithBot.coe_mul_eq_bind {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : α} (ha : a ≠ 0) (b : WithBot α) :
                                ↑a * b = Option.bind b fun (b : α) => Option.some (a * b)
                                source
                                @[simp]
                                theorem WithBot.unbotD_zero_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a b : WithBot α) :
                                unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
                                source
                                @[deprecated WithBot.unbotD_zero_mul (since := "2025-02-06")]
                                theorem WithBot.unbot'_zero_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a b : WithBot α) :
                                unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

                                Alias of WithBot.unbotD_zero_mul.

                                source
                                theorem WithBot.mul_ne_bot {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a b : WithBot α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) :
                                a * b ≠ ⊥
                                source
                                theorem WithBot.bot_lt_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a b : WithBot α} (ha : ⊥ < a) (hb : ⊥ < b) :
                                ⊥ < a * b
                                source
                                instance WithBot.instNoZeroDivisors {α : Type u_1} [DecidableEq α] [MulZeroClass α] [NoZeroDivisors α] :
                                NoZeroDivisors (WithBot α)
                                source
                                instance WithBot.instMulZeroOneClass {α : Type u_1} [DecidableEq α] [MulZeroOneClass α] [Nontrivial α] :
                                MulZeroOneClass (WithBot α)

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

                                Equations
                                  source
                                  instance WithBot.instSemigroupWithZero {α : Type u_1} [DecidableEq α] [SemigroupWithZero α] [NoZeroDivisors α] :
                                  SemigroupWithZero (WithBot α)
                                  Equations
                                    source
                                    instance WithBot.instMonoidWithZero {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] :
                                    MonoidWithZero (WithBot α)
                                    Equations
                                      source
                                      @[simp]
                                      theorem WithBot.coe_pow {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] (a : α) (n : ℕ) :
                                      ↑(a ^ n) = ↑a ^ n
                                      source
                                      instance WithBot.instCommMonoidWithZero {α : Type u_1} [DecidableEq α] [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] :
                                      CommMonoidWithZero (WithBot α)
                                      Equations
                                        source
                                        instance WithBot.instCommSemiring {α : Type u_1} [DecidableEq α] [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] :
                                        CommSemiring (WithBot α)
                                        Equations
                                          source
                                          instance WithBot.instPosMulMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulMono α] :
                                          PosMulMono (WithBot α)
                                          source
                                          instance WithBot.instMulPosMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosMono α] :
                                          MulPosMono (WithBot α)
                                          source
                                          instance WithBot.instPosMulStrictMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulStrictMono α] :
                                          PosMulStrictMono (WithBot α)
                                          source
                                          instance WithBot.instMulPosStrictMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosStrictMono α] :
                                          MulPosStrictMono (WithBot α)
                                          source
                                          instance WithBot.instPosMulReflectLT {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulReflectLT α] :
                                          PosMulReflectLT (WithBot α)
                                          source
                                          instance WithBot.instMulPosReflectLT {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosReflectLT α] :
                                          MulPosReflectLT (WithBot α)
                                          source
                                          instance WithBot.instPosMulReflectLE {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulReflectLE α] :
                                          PosMulReflectLE (WithBot α)
                                          source
                                          instance WithBot.instMulPosReflectLE {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosReflectLE α] :
                                          MulPosReflectLE (WithBot α)
                                          source
                                          instance WithBot.instIsOrderedRing {α : Type u_1} [DecidableEq α] [CommSemiring α] [PartialOrder α] [IsOrderedRing α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] :
                                          IsOrderedRing (WithBot α)