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).

Order dual #

source
@[implicit_reducible]
instance instNatCastOrderDual {α : Type u_1} [h : NatCast α] :
NatCast αᵒᵈ
Equations
source
@[implicit_reducible]
instance instAddMonoidWithOneOrderDual {α : Type u_1} [h : AddMonoidWithOne α] :
AddMonoidWithOne αᵒᵈ
Equations
source
@[implicit_reducible]
instance instAddCommMonoidWithOneOrderDual {α : Type u_1} [h : AddCommMonoidWithOne α] :
AddCommMonoidWithOne αᵒᵈ
Equations
source
@[simp]
theorem toDual_natCast {α : Type u_1} [NatCast α] (n : ℕ) :
OrderDual.toDual ↑n = ↑n
source
@[simp]
theorem toDual_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [n.AtLeastTwo] :
OrderDual.toDual (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem ofDual_natCast {α : Type u_1} [NatCast α] (n : ℕ) :
OrderDual.ofDual ↑n = ↑n
source
@[simp]
theorem ofDual_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [n.AtLeastTwo] :
OrderDual.ofDual (OfNat.ofNat n) = OfNat.ofNat n

Lexicographic order #

source
@[implicit_reducible]
instance instNatCastLex {α : Type u_1} [h : NatCast α] :
NatCast (Lex α)
Equations
source
@[implicit_reducible]
instance instAddMonoidWithOneLex {α : Type u_1} [h : AddMonoidWithOne α] :
AddMonoidWithOne (Lex α)
Equations
source
@[implicit_reducible]
instance instAddCommMonoidWithOneLex {α : Type u_1} [h : AddCommMonoidWithOne α] :
AddCommMonoidWithOne (Lex α)
Equations
source
@[simp]
theorem toLex_natCast {α : Type u_1} [NatCast α] (n : ℕ) :
toLex ↑n = ↑n
source
@[simp]
theorem toLex_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [n.AtLeastTwo] :
toLex (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem ofLex_natCast {α : Type u_1} [NatCast α] (n : ℕ) :
ofLex ↑n = ↑n
source
@[simp]
theorem ofLex_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [n.AtLeastTwo] :
ofLex (OfNat.ofNat n) = OfNat.ofNat n