Documentation

Mathlib.Data.Nat.Cast.Order.Ring

Cast of natural numbers: lemmas about bundled ordered semirings #

source
@[simp]
theorem Nat.cast_nonneg {α : Type u_3} [Semiring α] [PartialOrder α] [IsOrderedRing α] (n : ℕ) :
0 ≤ ↑n

Specialisation of Nat.cast_nonneg', which seems to be easier for Lean to use.

source
@[simp]
theorem Nat.ofNat_nonneg {α : Type u_3} [Semiring α] [PartialOrder α] [IsOrderedRing α] (n : ℕ) [n.AtLeastTwo] :
0 ≤ OfNat.ofNat n

Specialisation of Nat.ofNat_nonneg', which seems to be easier for Lean to use.

source
@[simp]
theorem Nat.cast_min {α : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] (m n : ℕ) :
↑(m ⊓ n) = ↑m ⊓ ↑n
source
@[simp]
theorem Nat.cast_max {α : Type u_3} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] (m n : ℕ) :
↑(m ⊔ n) = ↑m ⊔ ↑n
source
@[simp]
theorem Nat.cast_pos {α : Type u_3} [Semiring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α] {n : ℕ} :
0 < ↑n ↔ 0 < n

Specialisation of Nat.cast_pos', which seems to be easier for Lean to use.

source
@[simp]
theorem Nat.ofNat_pos' {α : Type u_2} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [NeZero 1] {n : ℕ} [n.AtLeastTwo] :
0 < OfNat.ofNat n

See also Nat.ofNat_pos, specialised for an OrderedSemiring.

source
@[simp]
theorem Nat.ofNat_pos {α : Type u_3} [Semiring α] [PartialOrder α] [IsOrderedRing α] [Nontrivial α] {n : ℕ} [n.AtLeastTwo] :
0 < OfNat.ofNat n

Specialisation of Nat.ofNat_pos', which seems to be easier for Lean to use.

source
@[simp]
theorem Nat.cast_tsub {α : Type u_2} [CommSemiring α] [PartialOrder α] [IsOrderedRing α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] (m n : ℕ) :
↑(m - n) = ↑m - ↑n

A version of Nat.cast_sub that works for ℝ≥0 and ℚ≥0. Note that this proof doesn't work for ℕ∞ and ℝ≥0∞, so we use type-specific lemmas for these types.

source
@[simp]
theorem Nat.abs_cast {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (n : ℕ) :
|↑n| = ↑n
source
@[simp]
theorem Nat.abs_ofNat {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] (n : ℕ) [n.AtLeastTwo] :
|OfNat.ofNat n| = OfNat.ofNat n
source
@[simp]
theorem Nat.neg_cast_eq_cast {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {m n : ℕ} :
-↑m = ↑n ↔ m = 0 ∧ n = 0
source
@[simp]
theorem Nat.cast_eq_neg_cast {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {m n : ℕ} :
↑m = -↑n ↔ m = 0 ∧ n = 0
source
theorem Nat.mul_le_pow {a : ℕ} (ha : a ≠ 1) (b : ℕ) :
a * b ≤ a ^ b
source
theorem Nat.two_mul_sq_add_one_le_two_pow_two_mul (k : ℕ) :
2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)