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 an AddMonoidHom.
• castRingHom: cast bundled as a RingHom.

Order dual

instance instNatCastOrderDual {α : Type u_1} [h : NatCast α] : NatCast αᵒᵈ

instance instAddMonoidWithOneOrderDual {α : Type u_1} [h : AddMonoidWithOne α] : AddMonoidWithOne αᵒᵈ

instance instAddCommMonoidWithOneOrderDual {α : Type u_1} [h : AddCommMonoidWithOne α] : AddCommMonoidWithOne αᵒᵈ

@[simp]

theorem toDual_natCast {α : Type u_1} [NatCast α] (n : ℕ) : ↑OrderDual.toDual ↑n = ↑n

@[simp]

theorem ofDual_natCast {α : Type u_1} [NatCast α] (n : ℕ) : ↑(↑OrderDual.ofDual n) = ↑n

Lexicographic order

instance instNatCastLex {α : Type u_1} [h : NatCast α] : NatCast (Lex α)

instance instAddMonoidWithOneLex {α : Type u_1} [h : AddMonoidWithOne α] : AddMonoidWithOne (Lex α)

instance instAddCommMonoidWithOneLex {α : Type u_1} [h : AddCommMonoidWithOne α] : AddCommMonoidWithOne (Lex α)

@[simp]

theorem toLex_natCast {α : Type u_1} [NatCast α] (n : ℕ) : ↑toLex ↑n = ↑n

@[simp]

theorem ofLex_natCast {α : Type u_1} [NatCast α] (n : ℕ) : ↑(↑ofLex n) = ↑n