Documentation

Mathlib.Tactic.Ring.PNat

Additional instances for ring over PNat #

This adds some instances which enable ring to work on PNat even though it is not a commutative semiring, by lifting to Nat.

source
instance Mathlib.Tactic.Ring.instCSLiftPNatNat :
CSLift ℕ+ ℕ
Equations
    source
    instance Mathlib.Tactic.Ring.instCSLiftValPNatNatOfNatHAdd {n : ℕ} :
    CSLiftVal (OfNat.ofNat (n + 1)) (n + 1)
    source
    instance Mathlib.Tactic.Ring.instCSLiftValPNatNatToPNat {n : ℕ} {h : 0 < n} :
    CSLiftVal (n.toPNat h) n
    source
    instance Mathlib.Tactic.Ring.instCSLiftValPNatNatSuccPNatHAddOfNat {n : ℕ} :
    CSLiftVal n.succPNat (n + 1)
    source
    instance Mathlib.Tactic.Ring.instCSLiftValPNatNatToPNat'HAddPredOfNat {n : ℕ} :
    CSLiftVal n.toPNat' (n.pred + 1)
    source
    instance Mathlib.Tactic.Ring.instCSLiftValPNatNatDivExactHAddDivOfNat {n k : ℕ+} :
    CSLiftVal (n.divExact k) (n.div k + 1)
    source
    instance Mathlib.Tactic.Ring.instCSLiftValPNatNatHAdd {n : ℕ+} {n' : ℕ} {k : ℕ+} {k' : ℕ} [h1 : CSLiftVal n n'] [h2 : CSLiftVal k k'] :
    CSLiftVal (n + k) (n' + k')
    source
    instance Mathlib.Tactic.Ring.instCSLiftValPNatNatHMul {n : ℕ+} {n' : ℕ} {k : ℕ+} {k' : ℕ} [h1 : CSLiftVal n n'] [h2 : CSLiftVal k k'] :
    CSLiftVal (n * k) (n' * k')
    source
    instance Mathlib.Tactic.Ring.instCSLiftValPNatNatHPow {n : ℕ+} {n' k : ℕ} [h1 : CSLiftVal n n'] :
    CSLiftVal (n ^ k) (n' ^ k)