Cast of natural numbers: lemmas about bundled ordered semirings #
@[simp]
Specialisation of Nat.cast_nonneg', which seems to be easier for Lean to use.
@[simp]
theorem
Nat.ofNat_nonneg
{α : Type u_2}
[OrderedSemiring α]
(n : ℕ)
[n.AtLeastTwo]
:
0 ≤ OfNat.ofNat n
Specialisation of Nat.ofNat_nonneg', which seems to be easier for Lean to use.
@[simp]
@[simp]
@[simp]
Specialisation of Nat.cast_pos', which seems to be easier for Lean to use.
@[simp]
theorem
Nat.ofNat_pos'
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[ZeroLEOneClass α]
[NeZero 1]
{n : ℕ}
[n.AtLeastTwo]
:
0 < OfNat.ofNat n
See also Nat.ofNat_pos, specialised for an OrderedSemiring.
@[simp]
theorem
Nat.ofNat_pos
{α : Type u_2}
[OrderedSemiring α]
[Nontrivial α]
{n : ℕ}
[n.AtLeastTwo]
:
0 < OfNat.ofNat n
Specialisation of Nat.ofNat_pos', which seems to be easier for Lean to use.
@[simp]
theorem
Nat.cast_tsub
{α : Type u_1}
[CanonicallyOrderedCommSemiring α]
[Sub α]
[OrderedSub α]
[ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
(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.
@[simp]
theorem
Nat.abs_ofNat
{α : Type u_1}
[LinearOrderedRing α]
(n : ℕ)
[n.AtLeastTwo]
:
|OfNat.ofNat n| = OfNat.ofNat n