# Documentation

Mathlib.Data.Nat.Cast.Synonym

# 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 : ] :
instance instAddMonoidWithOneOrderDual {α : Type u_1} [h : ] :
instance instAddCommMonoidWithOneOrderDual {α : Type u_1} [h : ] :
@[simp]
theorem toDual_natCast {α : Type u_1} [] (n : ) :
OrderDual.toDual n = n
@[simp]
theorem ofDual_natCast {α : Type u_1} [] (n : ) :
↑(OrderDual.ofDual n) = n

### Lexicographic order #

instance instNatCastLex {α : Type u_1} [h : ] :
instance instAddMonoidWithOneLex {α : Type u_1} [h : ] :
instance instAddCommMonoidWithOneLex {α : Type u_1} [h : ] :
@[simp]
theorem toLex_natCast {α : Type u_1} [] (n : ) :
toLex n = n
@[simp]
theorem ofLex_natCast {α : Type u_1} [] (n : ) :
↑(ofLex n) = n