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

Lexicographic order

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[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