# 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

- Mathlib.Tactic.Ring.instCSLiftPNatNat = { lift := PNat.val, inj := PNat.coe_injective }

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)