Documentation

Mathlib.Data.ENat.Monoid

LinearOrderedAddCommMonoidWithTop structure on ENat #

source
@[instance_reducible]
instance instLinearOrderedAddCommMonoidWithTopENat :
LinearOrderedAddCommMonoidWithTop ℕ∞
Equations
  • One or more equations did not get rendered due to their size.
source
instance instIsOrderedRingENat :
IsOrderedRing ℕ∞
source
instance instCanonicallyOrderedAddENat :
CanonicallyOrderedAdd ℕ∞
source
instance instCharZeroENat :
CharZero ℕ∞
source
@[instance_reducible]
instance instCommSemiringENat :
CommSemiring ℕ∞
Equations
  • One or more equations did not get rendered due to their size.
source
instance instOrderedSubENat :
OrderedSub ℕ∞
source
@[instance_reducible]
instance instAddMonoidWithOneENat :
AddMonoidWithOne ℕ∞
Equations
  • One or more equations did not get rendered due to their size.
source
instance instNoZeroDivisorsENat :
NoZeroDivisors ℕ∞
source
@[simp]
theorem ENat.natCast_mul (m n : ℕ) :
↑(m * n) = ↑m * ↑n
source
@[deprecated ENat.natCast_mul (since := "2026-07-17")]
theorem ENat.coe_mul (m n : ℕ) :
↑(m * n) = ↑m * ↑n

Alias of ENat.natCast_mul.

source
@[simp]
theorem ENat.mul_top {m : ℕ∞} (hm : m ≠ 0) :
m * ⊤ = ⊤
source
@[simp]
theorem ENat.top_mul {m : ℕ∞} (hm : m ≠ 0) :
⊤ * m = ⊤
source
theorem ENat.mul_top' {m : ℕ∞} :
m * ⊤ = if m = 0 then 0 else ⊤

A version of mul_top where the RHS is stated as an ite

source
theorem ENat.top_mul' {m : ℕ∞} :
⊤ * m = if m = 0 then 0 else ⊤

A version of top_mul where the RHS is stated as an ite

source
@[simp]
theorem ENat.top_pow {n : ℕ} (hn : n ≠ 0) :
⊤ ^ n = ⊤
source
@[simp]
theorem ENat.pow_eq_top_iff {a : ℕ∞} {n : ℕ} :
a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0
source
theorem ENat.pow_ne_top_iff {a : ℕ∞} {n : ℕ} :
a ^ n ≠ ⊤ ↔ a ≠ ⊤ ∨ n = 0
source
@[simp]
theorem ENat.pow_lt_top_iff {a : ℕ∞} {n : ℕ} :
a ^ n < ⊤ ↔ a < ⊤ ∨ n = 0
source
theorem ENat.eq_top_of_pow {a : ℕ∞} (n : ℕ) (ha : a ^ n = ⊤) :
a = ⊤
source
@[simp]
theorem ENat.lift_add (a b : ℕ∞) (h : a + b < ⊤) :
(a + b).lift h = a.lift ⋯ + b.lift ⋯
source
def ENat.toNatHom :
ℕ∞ →*₀ ℕ

Homomorphism from ℕ∞ to ℕ sending ∞ to 0.

Equations
Instances For
    source
    @[simp]
    theorem ENat.coe_toNatHom :
    ⇑toNatHom = toNat
    source
    theorem ENat.toNatHom_apply (n : ℕ) :
    toNatHom ↑n = (↑n).toNat
    source
    @[simp]
    theorem ENat.natCast_toNat_eq_self {n : ℕ∞} :
    ↑n.toNat = n ↔ n ≠ ⊤
    source
    @[deprecated ENat.natCast_toNat_eq_self (since := "2026-07-17")]
    theorem ENat.coe_toNat_eq_self {n : ℕ∞} :
    ↑n.toNat = n ↔ n ≠ ⊤

    Alias of ENat.natCast_toNat_eq_self.

    source
    theorem ENat.natCast_toNat {n : ℕ∞} :
    n ≠ ⊤ → ↑n.toNat = n

    Alias of the reverse direction of ENat.natCast_toNat_eq_self.

    source
    @[deprecated ENat.natCast_toNat (since := "2026-07-17")]
    theorem ENat.coe_toNat {n : ℕ∞} :
    n ≠ ⊤ → ↑n.toNat = n

    Alias of ENat.natCast_toNat.

    Alias of the reverse direction of ENat.natCast_toNat_eq_self.

    source
    @[simp]
    theorem ENat.toNat_eq_iff_eq_natCast (n : ℕ∞) (m : ℕ) [NeZero m] :
    n.toNat = m ↔ n = ↑m
    source
    @[simp]
    theorem ENat.toNat_mul (a b : ℕ∞) :
    (a * b).toNat = a.toNat * b.toNat
    source
    theorem ENat.toNat_eq_iff {m : ℕ∞} {n : ℕ} (hn : n ≠ 0) :
    m.toNat = n ↔ m = ↑n
    source
    theorem ENat.toNat_le_of_le_natCast {m : ℕ∞} {n : ℕ} (h : m ≤ ↑n) :
    m.toNat ≤ n
    source
    @[deprecated ENat.toNat_le_of_le_natCast (since := "2026-07-17")]
    theorem ENat.toNat_le_of_le_coe {m : ℕ∞} {n : ℕ} (h : m ≤ ↑n) :
    m.toNat ≤ n

    Alias of ENat.toNat_le_of_le_natCast.

    source
    theorem ENat.toNat_le_toNat {m n : ℕ∞} (h : m ≤ n) (hn : n ≠ ⊤) :
    m.toNat ≤ n.toNat
    source
    @[deprecated ENat.toNat_eq_iff_eq_natCast (since := "2026-07-17")]
    theorem ENat.toNat_eq_iff_eq_coe (n : ℕ∞) (m : ℕ) [NeZero m] :
    n.toNat = m ↔ n = ↑m

    Alias of ENat.toNat_eq_iff_eq_natCast.

    source
    @[deprecated add_pos_of_right (since := "2026-05-25")]
    theorem ENat.add_one_pos {n : ℕ∞} :
    0 < n + 1
    source
    theorem ENat.natCast_lt_succ {n : ℕ} :
    ↑n < ↑n + 1
    source
    theorem ENat.le_sub_of_add_le_left {a b c : ℕ∞} (ha : a ≠ ⊤) :
    a + b ≤ c → b ≤ c - a
    source
    theorem ENat.le_sub_of_add_le_right {a b c : ℕ∞} (hb : b ≠ ⊤) :
    a + b ≤ c → a ≤ c - b
    source
    theorem ENat.lt_add_left {n k : ℕ∞} (h : n ≠ ⊤) (h' : 0 < k) :
    n < k + n
    source
    theorem ENat.sub_sub_cancel {a b : ℕ∞} (h : a ≠ ⊤) (h2 : b ≤ a) :
    a - (a - b) = b
    source
    theorem ENat.add_left_injective_of_ne_top {n : ℕ∞} (hn : n ≠ ⊤) :
    Function.Injective fun (x : ℕ∞) => x + n
    source
    theorem ENat.add_right_injective_of_ne_top {n : ℕ∞} (hn : n ≠ ⊤) :
    Function.Injective fun (x : ℕ∞) => n + x
    source
    theorem ENat.mul_right_strictMono {a : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) :
    StrictMono fun (x : ℕ∞) => a * x
    source
    theorem ENat.mul_left_strictMono {a : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) :
    StrictMono fun (x : ℕ∞) => x * a
    source
    @[simp]
    theorem ENat.mul_le_mul_left_iff {a x y : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) :
    a * x ≤ a * y ↔ x ≤ y
    source
    @[simp]
    theorem ENat.mul_le_mul_right_iff {a x y : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) :
    x * a ≤ y * a ↔ x ≤ y
    source
    theorem ENat.mul_le_mul_of_le_right {a x y : ℕ∞} (hxy : x ≤ y) (ha : a ≠ 0) (h_top : a ≠ ⊤) :
    x * a ≤ y * a
    source
    theorem ENat.self_le_mul_right {c : ℕ∞} (a : ℕ∞) (hc : c ≠ 0) :
    a ≤ a * c
    source
    theorem ENat.self_le_mul_left {c : ℕ∞} (a : ℕ∞) (hc : c ≠ 0) :
    a ≤ c * a
    source
    @[instance_reducible]
    instance ENat.instUniqueUnits :
    Unique ℕ∞ˣ
    Equations
    source
    theorem ENat.add_one_natCast_le_withTop_of_lt {m : ℕ} {n : WithTop ℕ∞} (h : ↑m < n) :
    ↑(m + 1) ≤ n
    source
    @[simp]
    theorem ENat.coe_top_add_one :
    ↑⊤ + 1 = ↑⊤
    source
    @[simp]
    theorem ENat.add_one_eq_coe_top_iff {n : WithTop ℕ∞} :
    n + 1 = ↑⊤ ↔ n = ↑⊤
    source
    @[simp]
    theorem ENat.natCast_ne_coe_top (n : ℕ) :
    ↑n ≠ ↑⊤
    source
    theorem ENat.one_le_iff_ne_zero_withTop {n : WithTop ℕ∞} :
    1 ≤ n ↔ n ≠ 0
    source
    theorem ENat.natCast_le_of_coe_top_le_withTop {N : WithTop ℕ∞} (hN : ↑⊤ ≤ N) (n : ℕ) :
    ↑n ≤ N
    source
    theorem ENat.natCast_lt_of_coe_top_le_withTop {N : WithTop ℕ∞} (hN : ↑⊤ ≤ N) (n : ℕ) :
    ↑n < N
    source
    @[simp]
    theorem ENat.map_natCast_nonneg {n : ℕ∞} {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] :
    0 ≤ map Nat.cast n
    source
    theorem ENat.map_natCast_strictMono {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] :
    StrictMono (map Nat.cast)
    source
    theorem ENat.map_natCast_injective {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] :
    Function.Injective (map Nat.cast)
    source
    @[simp]
    theorem ENat.map_natCast_inj {m n : ℕ∞} {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] :
    map Nat.cast m = map Nat.cast n ↔ m = n
    source
    @[simp]
    theorem ENat.map_natCast_eq_zero {n : ℕ∞} {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] :
    map Nat.cast n = 0 ↔ n = 0
    source
    def AddMonoidHom.ENatMap {N : Type u_1} [AddZeroClass N] (f : ℕ →+ N) :
    ℕ∞ →+ WithTop N

    A version of WithTop.map for AddMonoidHoms.

    Equations
    Instances For
      source
      @[simp]
      theorem AddMonoidHom.ENatMap_apply {N : Type u_1} [AddZeroClass N] (f : ℕ →+ N) :
      ⇑f.ENatMap = ENat.map ⇑f
      source
      def MonoidWithZeroHom.ENatMap {S : Type u_1} [MulZeroOneClass S] [DecidableEq S] [Nontrivial S] (f : ℕ →*₀ S) (hf : Function.Injective ⇑f) :
      ℕ∞ →*₀ WithTop S

      A version of ENat.map for MonoidWithZeroHoms.

      Equations
      • f.ENatMap hf = { toFun := ENat.map ⇑f, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
      Instances For
        source
        @[simp]
        theorem MonoidWithZeroHom.ENatMap_apply {S : Type u_1} [MulZeroOneClass S] [DecidableEq S] [Nontrivial S] (f : ℕ →*₀ S) (hf : Function.Injective ⇑f) :
        ⇑(f.ENatMap hf) = ENat.map ⇑f
        source
        def RingHom.ENatMap {S : Type u_1} [CommSemiring S] [PartialOrder S] [CanonicallyOrderedAdd S] [DecidableEq S] [Nontrivial S] (f : ℕ →+* S) (hf : Function.Injective ⇑f) :
        ℕ∞ →+* WithTop S

        A version of ENat.map for RingHoms.

        Equations
        Instances For
          source
          @[simp]
          theorem RingHom.ENatMap_apply {S : Type u_1} [CommSemiring S] [PartialOrder S] [CanonicallyOrderedAdd S] [DecidableEq S] [Nontrivial S] (f : ℕ →+* S) (hf : Function.Injective ⇑f) :
          ⇑(f.ENatMap hf) = (↑(f.toMonoidWithZeroHom.ENatMap hf)).toFun
          source
          @[simp]
          theorem ENat.map_natCast_mul {R : Type u_1} [NonAssocSemiring R] [DecidableEq R] [CharZero R] (a b : ℕ∞) :
          map Nat.cast (a * b) = map Nat.cast a * map Nat.cast b
          source
          @[simp]
          theorem ENat.WithBot.add_natCast_cancel {a b : WithBot ℕ∞} {c : ℕ} :
          a + ↑c = b + ↑c ↔ a = b
          source
          @[simp]
          theorem ENat.WithBot.add_one_cancel {a b : WithBot ℕ∞} :
          a + 1 = b + 1 ↔ a = b
          source
          theorem ENat.WithBot.add_ofNat_cancel {a b : WithBot ℕ∞} {c : ℕ} [c.AtLeastTwo] :
          a + OfNat.ofNat c = b + OfNat.ofNat c ↔ a = b
          source
          @[simp]
          theorem ENat.WithBot.natCast_add_cancel {a b : WithBot ℕ∞} {c : ℕ} :
          ↑c + a = ↑c + b ↔ a = b
          source
          @[simp]
          theorem ENat.WithBot.one_add_cancel {a b : WithBot ℕ∞} :
          1 + a = 1 + b ↔ a = b
          source
          theorem ENat.WithBot.ofNat_add_cancel {a b : WithBot ℕ∞} {c : ℕ} [c.AtLeastTwo] :
          OfNat.ofNat c + a = OfNat.ofNat c + b ↔ a = b
          source
          theorem ENat.WithBot.add_le_add_natCast_right_iff {a b : WithBot ℕ∞} {c : ℕ} :
          a + ↑c ≤ b + ↑c ↔ a ≤ b
          source
          theorem ENat.WithBot.add_le_add_one_right_iff {a b : WithBot ℕ∞} :
          a + 1 ≤ b + 1 ↔ a ≤ b
          source
          theorem ENat.WithBot.add_le_add_natCast_left_iff {a b : WithBot ℕ∞} {c : ℕ} :
          ↑c + a ≤ ↑c + b ↔ a ≤ b
          source
          theorem ENat.WithBot.add_le_add_one_left_iff {a b : WithBot ℕ∞} :
          1 + a ≤ 1 + b ↔ a ≤ b