LinearOrderedAddCommMonoidWithTop structure on ENat

@[instance_reducible]

instance instLinearOrderedAddCommMonoidWithTopENat : LinearOrderedAddCommMonoidWithTop ℕ∞

Equations

• One or more equations did not get rendered due to their size.

instance instIsOrderedRingENat : IsOrderedRing ℕ∞

instance instCanonicallyOrderedAddENat : CanonicallyOrderedAdd ℕ∞

instance instCharZeroENat : CharZero ℕ∞

@[instance_reducible]

instance instCommSemiringENat : CommSemiring ℕ∞

Equations

• One or more equations did not get rendered due to their size.

instance instOrderedSubENat : OrderedSub ℕ∞

@[instance_reducible]

instance instAddMonoidWithOneENat : AddMonoidWithOne ℕ∞

Equations

• One or more equations did not get rendered due to their size.

instance instNoZeroDivisorsENat : NoZeroDivisors ℕ∞

@[simp]

theorem ENat.natCast_mul (m n : ℕ) : ↑(m * n) = ↑m * ↑n

@[deprecated ENat.natCast_mul (since := "2026-07-17")]

theorem ENat.coe_mul (m n : ℕ) : ↑(m * n) = ↑m * ↑n

Alias of ENat.natCast_mul.

@[simp]

theorem ENat.mul_top {m : ℕ∞} (hm : m ≠ 0) : m * ⊤ = ⊤

@[simp]

theorem ENat.top_mul {m : ℕ∞} (hm : m ≠ 0) : ⊤ * m = ⊤

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

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

@[simp]

theorem ENat.top_pow {n : ℕ} (hn : n ≠ 0) : ⊤ ^ n = ⊤

@[simp]

theorem ENat.pow_eq_top_iff {a : ℕ∞} {n : ℕ} : a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0

theorem ENat.pow_ne_top_iff {a : ℕ∞} {n : ℕ} : a ^ n ≠ ⊤ ↔ a ≠ ⊤ ∨ n = 0

@[simp]

theorem ENat.pow_lt_top_iff {a : ℕ∞} {n : ℕ} : a ^ n < ⊤ ↔ a < ⊤ ∨ n = 0

theorem ENat.eq_top_of_pow {a : ℕ∞} (n : ℕ) (ha : a ^ n = ⊤) : a = ⊤

@[simp]

theorem ENat.lift_add (a b : ℕ∞) (h : a + b < ⊤) : (a + b).lift h = a.lift ⋯ + b.lift ⋯

def ENat.toNatHom : ℕ∞ →*₀ ℕ

Homomorphism from ℕ∞ to ℕ sending ∞ to 0.

Equations

• ENat.toNatHom = { toFun := ENat.toNat, map_zero' := ENat.toNatHom._proof_1, map_one' := ENat.toNatHom._proof_2, map_mul' := ⋯ }

@[simp]

theorem ENat.coe_toNatHom : ⇑toNatHom = toNat

theorem ENat.toNatHom_apply (n : ℕ) : toNatHom ↑n = (↑n).toNat

@[simp]

theorem ENat.toNat_mul (a b : ℕ∞) : (a * b).toNat = a.toNat * b.toNat

@[deprecated add_pos_of_right (since := "2026-05-25")]

theorem ENat.add_one_pos {n : ℕ∞} : 0 < n + 1

theorem ENat.natCast_lt_succ {n : ℕ} : ↑n < ↑n + 1

theorem ENat.le_sub_of_add_le_left {a b c : ℕ∞} (ha : a ≠ ⊤) : a + b ≤ c → b ≤ c - a

theorem ENat.le_sub_of_add_le_right {a b c : ℕ∞} (hb : b ≠ ⊤) : a + b ≤ c → a ≤ c - b

theorem ENat.lt_add_left {n k : ℕ∞} (h : n ≠ ⊤) (h' : 0 < k) : n < k + n

theorem ENat.sub_sub_cancel {a b : ℕ∞} (h : a ≠ ⊤) (h2 : b ≤ a) : a - (a - b) = b

theorem ENat.add_left_injective_of_ne_top {n : ℕ∞} (hn : n ≠ ⊤) : Function.Injective fun (x : ℕ∞) => x + n

theorem ENat.add_right_injective_of_ne_top {n : ℕ∞} (hn : n ≠ ⊤) : Function.Injective fun (x : ℕ∞) => n + x

theorem ENat.mul_right_strictMono {a : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) : StrictMono fun (x : ℕ∞) => a * x

theorem ENat.mul_left_strictMono {a : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) : StrictMono fun (x : ℕ∞) => x * a

@[simp]

theorem ENat.mul_le_mul_left_iff {a x y : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) : a * x ≤ a * y ↔ x ≤ y

@[simp]

theorem ENat.mul_le_mul_right_iff {a x y : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) : x * a ≤ y * a ↔ x ≤ y

theorem ENat.mul_le_mul_of_le_right {a x y : ℕ∞} (hxy : x ≤ y) (ha : a ≠ 0) (h_top : a ≠ ⊤) : x * a ≤ y * a

theorem ENat.self_le_mul_right {c : ℕ∞} (a : ℕ∞) (hc : c ≠ 0) : a ≤ a * c

theorem ENat.self_le_mul_left {c : ℕ∞} (a : ℕ∞) (hc : c ≠ 0) : a ≤ c * a

@[instance_reducible]

instance ENat.instUniqueUnits : Unique ℕ∞ˣ

Equations

• ENat.instUniqueUnits = { toInhabited := Units.instInhabited, uniq := ⋯ }

theorem ENat.add_one_natCast_le_withTop_of_lt {m : ℕ} {n : WithTop ℕ∞} (h : ↑m < n) : ↑(m + 1) ≤ n

@[simp]

theorem ENat.coe_top_add_one : ↑⊤ + 1 = ↑⊤

@[simp]

theorem ENat.add_one_eq_coe_top_iff {n : WithTop ℕ∞} : n + 1 = ↑⊤ ↔ n = ↑⊤

@[simp]

theorem ENat.natCast_ne_coe_top (n : ℕ) : ↑n ≠ ↑⊤

theorem ENat.one_le_iff_ne_zero_withTop {n : WithTop ℕ∞} : 1 ≤ n ↔ n ≠ 0

theorem ENat.natCast_le_of_coe_top_le_withTop {N : WithTop ℕ∞} (hN : ↑⊤ ≤ N) (n : ℕ) : ↑n ≤ N

theorem ENat.natCast_lt_of_coe_top_le_withTop {N : WithTop ℕ∞} (hN : ↑⊤ ≤ N) (n : ℕ) : ↑n < N

@[simp]

theorem ENat.map_natCast_nonneg {n : ℕ∞} {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] : 0 ≤ map Nat.cast n

theorem ENat.map_natCast_strictMono {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] : StrictMono (map Nat.cast)

theorem ENat.map_natCast_injective {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] : Function.Injective (map Nat.cast)

@[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

@[simp]

theorem ENat.map_natCast_eq_zero {n : ℕ∞} {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] : map Nat.cast n = 0 ↔ n = 0

def AddMonoidHom.ENatMap {N : Type u_1} [AddZeroClass N] (f : ℕ →+ N) : ℕ∞ →+ WithTop N

A version of WithTop.map for AddMonoidHoms.

Equations

• f.ENatMap = { toFun := ENat.map ⇑f, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidHom.ENatMap_apply {N : Type u_1} [AddZeroClass N] (f : ℕ →+ N) : ⇑f.ENatMap = ENat.map ⇑f

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' := ⋯ }

@[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

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

• f.ENatMap hf = { toFun := (↑((↑f).ENatMap hf)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[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).ENatMap hf)).toFun

@[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

@[simp]

theorem ENat.WithBot.add_natCast_cancel {a b : WithBot ℕ∞} {c : ℕ} : a + ↑c = b + ↑c ↔ a = b

@[simp]

theorem ENat.WithBot.add_one_cancel {a b : WithBot ℕ∞} : a + 1 = b + 1 ↔ a = b

theorem ENat.WithBot.add_ofNat_cancel {a b : WithBot ℕ∞} {c : ℕ} [c.AtLeastTwo] : a + OfNat.ofNat c = b + OfNat.ofNat c ↔ a = b

@[simp]

theorem ENat.WithBot.natCast_add_cancel {a b : WithBot ℕ∞} {c : ℕ} : ↑c + a = ↑c + b ↔ a = b

@[simp]

theorem ENat.WithBot.one_add_cancel {a b : WithBot ℕ∞} : 1 + a = 1 + b ↔ a = b

theorem ENat.WithBot.ofNat_add_cancel {a b : WithBot ℕ∞} {c : ℕ} [c.AtLeastTwo] : OfNat.ofNat c + a = OfNat.ofNat c + b ↔ a = b

theorem ENat.WithBot.add_le_add_natCast_right_iff {a b : WithBot ℕ∞} {c : ℕ} : a + ↑c ≤ b + ↑c ↔ a ≤ b

theorem ENat.WithBot.add_le_add_one_right_iff {a b : WithBot ℕ∞} : a + 1 ≤ b + 1 ↔ a ≤ b

theorem ENat.WithBot.add_le_add_natCast_left_iff {a b : WithBot ℕ∞} {c : ℕ} : ↑c + a ≤ ↑c + b ↔ a ≤ b

theorem ENat.WithBot.add_le_add_one_left_iff {a b : WithBot ℕ∞} : 1 + a ≤ 1 + b ↔ a ≤ b