Cast of natural numbers: lemmas about order #
theorem
Nat.mono_cast
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
:
Monotone Nat.cast
@[simp]
theorem
Nat.cast_nonneg'
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
(n : ℕ)
:
See also Nat.cast_nonneg, specialised for an OrderedSemiring.
@[simp]
theorem
Nat.ofNat_nonneg'
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
(n : ℕ)
[n.AtLeastTwo]
:
See also Nat.ofNat_nonneg, specialised for an OrderedSemiring.
theorem
Nat.cast_add_one_pos
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[NeZero 1]
(n : ℕ)
:
@[simp]
theorem
Nat.cast_pos'
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[NeZero 1]
{n : ℕ}
:
See also Nat.cast_pos, specialised for an OrderedSemiring.
theorem
Nat.strictMono_cast
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
:
StrictMono Nat.cast
def
Nat.castOrderEmbedding
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
:
Nat.cast : ℕ → α as an OrderEmbedding
Instances For
@[simp]
theorem
Nat.castOrderEmbedding_apply
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
:
⇑castOrderEmbedding = Nat.cast
@[simp]
theorem
Nat.cast_le
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{m n : ℕ}
:
@[simp]
theorem
Nat.cast_lt
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{m n : ℕ}
:
@[simp]
theorem
Nat.one_lt_cast
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{n : ℕ}
:
@[simp]
theorem
Nat.one_le_cast
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{n : ℕ}
:
theorem
Nat.one_le_cast_iff_ne_zero
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{n : ℕ}
:
1 ≤ ↑n ↔ n ≠ 0
@[simp]
theorem
Nat.cast_lt_one
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{n : ℕ}
:
↑n < 1 ↔ n = 0
@[simp]
theorem
Nat.cast_le_one
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{n : ℕ}
:
@[simp]
theorem
Nat.cast_nonpos
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{n : ℕ}
:
↑n ≤ 0 ↔ n = 0
@[simp]
theorem
Nat.ofNat_le_cast
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{m n : ℕ}
[m.AtLeastTwo]
:
@[simp]
theorem
Nat.ofNat_lt_cast
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{m n : ℕ}
[m.AtLeastTwo]
:
@[simp]
theorem
Nat.cast_le_ofNat
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{m n : ℕ}
[n.AtLeastTwo]
:
@[simp]
theorem
Nat.cast_lt_ofNat
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{m n : ℕ}
[n.AtLeastTwo]
:
@[simp]
theorem
Nat.one_lt_ofNat
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{n : ℕ}
[n.AtLeastTwo]
:
@[simp]
theorem
Nat.one_le_ofNat
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{n : ℕ}
[n.AtLeastTwo]
:
@[simp]
theorem
Nat.not_ofNat_le_one
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{n : ℕ}
[n.AtLeastTwo]
:
¬OfNat.ofNat n ≤ 1
@[simp]
theorem
Nat.not_ofNat_lt_one
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{n : ℕ}
[n.AtLeastTwo]
:
¬OfNat.ofNat n < 1
theorem
Nat.ofNat_le
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{m n : ℕ}
[n.AtLeastTwo]
[m.AtLeastTwo]
:
theorem
Nat.ofNat_lt
{α : Type u_1}
[AddMonoidWithOne α]
[PartialOrder α]
[AddLeftMono α]
[ZeroLEOneClass α]
[CharZero α]
{m n : ℕ}
[n.AtLeastTwo]
[m.AtLeastTwo]
:
theorem
NeZero.nat_of_injective
{R : Type u_2}
{S : Type u_3}
{F : Type u_4}
[NonAssocSemiring R]
[NonAssocSemiring S]
[FunLike F R S]
{n : ℕ}
[NeZero ↑n]
[RingHomClass F R S]
{f : F}
(hf : Function.Injective ⇑f)
:
NeZero ↑n