Cast of natural numbers (additional theorems) #
This file proves additional properties about the canonical homomorphism from
the natural numbers into an additive monoid with a one (Nat.cast
).
Main declarations #
castAddMonoidHom
:cast
bundled as anAddMonoidHom
.castRingHom
:cast
bundled as aRingHom
.
Nat.cast : ℕ → α→ α
as an AddMonoidHom
.
@[simp]
theorem
Nat.coe_castAddMonoidHom
{α : Type u_1}
[inst : AddMonoidWithOne α]
:
↑(Nat.castAddMonoidHom α) = Nat.cast
@[simp]
Nat.cast : ℕ → α→ α
as a RingHom
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Nat.coe_castRingHom
{α : Type u_1}
[inst : NonAssocSemiring α]
:
↑(Nat.castRingHom α) = Nat.cast
theorem
Nat.cast_add_one_pos
{α : Type u_1}
[inst : OrderedSemiring α]
[inst : Nontrivial α]
(n : ℕ)
:
@[simp]
theorem
Nat.strictMono_cast
{α : Type u_1}
[inst : OrderedSemiring α]
[inst : CharZero α]
:
StrictMono Nat.cast
@[simp]
theorem
Nat.castOrderEmbedding_apply
{α : Type u_1}
[inst : OrderedSemiring α]
[inst : CharZero α]
:
↑Nat.castOrderEmbedding.toEmbedding = Nat.cast
Nat.cast : ℕ → α→ α
as an OrderEmbedding
Equations
- Nat.castOrderEmbedding = OrderEmbedding.ofStrictMono Nat.cast (_ : StrictMono Nat.cast)
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Nat.cast_tsub
{α : Type u_1}
[inst : CanonicallyOrderedCommSemiring α]
[inst : Sub α]
[inst : OrderedSub α]
[inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
(m : ℕ)
(n : ℕ)
:
A version of Nat.cast_sub
that works for ℝ≥0≥0
and ℚ≥0≥0
. Note that this proof doesn't work
for ℕ∞∞
and ℝ≥0∞≥0∞∞
, so we use type-specific lemmas for these types.
@[simp]
@[simp]
@[simp]
Alias of Nat.coe_nat_dvd
.
Equations
theorem
eq_natCast'
{A : Type u_2}
{F : Type u_1}
[inst : AddMonoidWithOne A]
[inst : AddMonoidHomClass F ℕ A]
(f : F)
(h1 : ↑f 1 = 1)
(n : ℕ)
:
↑f n = ↑n
theorem
map_natCast'
{B : Type u_3}
{F : Type u_2}
[inst : AddMonoidWithOne B]
{A : Type u_1}
[inst : AddMonoidWithOne A]
[inst : AddMonoidHomClass F A B]
(f : F)
(h : ↑f 1 = 1)
(n : ℕ)
:
↑f ↑n = ↑n
theorem
ext_nat''
{A : Type u_2}
{F : Type u_1}
[inst : MulZeroOneClass A]
[inst : MonoidWithZeroHomClass F ℕ A]
(f : F)
(g : F)
(h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n)
:
f = g
If two MonoidWithZeroHom
s agree on the positive naturals they are equal.
@[simp]
theorem
eq_natCast
{R : Type u_2}
{F : Type u_1}
[inst : NonAssocSemiring R]
[inst : RingHomClass F ℕ R]
(f : F)
(n : ℕ)
:
↑f n = ↑n
@[simp]
theorem
map_natCast
{R : Type u_2}
{S : Type u_3}
{F : Type u_1}
[inst : NonAssocSemiring R]
[inst : NonAssocSemiring S]
[inst : RingHomClass F R S]
(f : F)
(n : ℕ)
:
↑f ↑n = ↑n
theorem
ext_nat
{R : Type u_2}
{F : Type u_1}
[inst : NonAssocSemiring R]
[inst : RingHomClass F ℕ R]
(f : F)
(g : F)
:
f = g
theorem
NeZero.nat_of_injective
{R : Type u_1}
{S : Type u_3}
{F : Type u_2}
[inst : NonAssocSemiring R]
[inst : NonAssocSemiring S]
{n : ℕ}
[h : NeZero ↑n]
[inst : RingHomClass F R S]
{f : F}
(hf : Function.Injective ↑f)
:
NeZero ↑n
theorem
RingHom.eq_natCast'
{R : Type u_1}
[inst : NonAssocSemiring R]
(f : ℕ →+* R)
:
f = Nat.castRingHom R
This is primed to match eq_intCast'
.
We don't use RingHomClass
here, since that might cause type-class slowdown for
Subsingleton
Equations
- Nat.uniqueRingHom = { toInhabited := { default := Nat.castRingHom R }, uniq := (_ : ∀ (f : ℕ →+* R), f = Nat.castRingHom R) }
Order dual #
Equations
- instAddMonoidWithOneOrderDual = h
Equations
- instAddCommMonoidWithOneOrderDual = h
Lexicographic order #
Equations
- instAddMonoidWithOneLex = h
Equations
- instAddCommMonoidWithOneLex = h