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 αᵒᵈ

Equations

• instNatCastOrderDual = h

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

Equations

• instAddMonoidWithOneOrderDual = h

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

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 α] : NatCast (Lex α)

Equations

• instNatCastLex = h

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

Equations

• instAddMonoidWithOneLex = h

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

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] : toLex (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

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

@[simp]

theorem ofLex_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [n.AtLeastTwo] : ofLex (OfNat.ofNat n) = OfNat.ofNat n