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
instance instNatCastOrderDual {α : Type u_1} [h : NatCast α] :
NatCast αᵒᵈ
Equations
    source
    instance instAddMonoidWithOneOrderDual {α : Type u_1} [h : AddMonoidWithOne α] :
    AddMonoidWithOne αᵒᵈ
    Equations
      source
      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
        instance instNatCastLex {α : Type u_1} [h : NatCast α] :
        NatCast (Lex α)
        Equations
          source
          instance instAddMonoidWithOneLex {α : Type u_1} [h : AddMonoidWithOne α] :
          AddMonoidWithOne (Lex α)
          Equations
            source
            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