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 #

Order dual #

instance instNatCastOrderDual {α : Type u_1} [h : NatCast α] :
Equations
  • instNatCastOrderDual = h
Equations
  • instAddMonoidWithOneOrderDual = h
Equations
  • instAddCommMonoidWithOneOrderDual = h
@[simp]
theorem toDual_natCast {α : Type u_1} [NatCast α] (n : ) :
OrderDual.toDual n = n
@[simp]
theorem toDual_ofNat {α : Type u_1} [NatCast α] (n : ) [n.AtLeastTwo] :
OrderDual.toDual (OfNat.ofNat n) = OfNat.ofNat n
@[simp]
theorem ofDual_natCast {α : Type u_1} [NatCast α] (n : ) :
OrderDual.ofDual n = n
@[simp]
theorem ofDual_ofNat {α : Type u_1} [NatCast α] (n : ) [n.AtLeastTwo] :
OrderDual.ofDual (OfNat.ofNat n) = OfNat.ofNat n

Lexicographic order #

instance instNatCastLex {α : Type u_1} [h : NatCast α] :
Equations
  • instNatCastLex = h
Equations
  • instAddMonoidWithOneLex = h
Equations
  • instAddCommMonoidWithOneLex = h
@[simp]
theorem toLex_natCast {α : Type u_1} [NatCast α] (n : ) :
toLex n = n
@[simp]
theorem toLex_ofNat {α : Type u_1} [NatCast α] (n : ) [n.AtLeastTwo] :
@[simp]
theorem ofLex_natCast {α : Type u_1} [NatCast α] (n : ) :
ofLex n = n
@[simp]
theorem ofLex_ofNat {α : Type u_1} [NatCast α] (n : ) [n.AtLeastTwo] :