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.

instance Mathlib.Tactic.Ring.instCSLiftPNatNat : CSLift ℕ+ ℕ

Equations

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

instance Mathlib.Tactic.Ring.instCSLiftValPNatNatOfNatHAdd {n : ℕ} : CSLiftVal (OfNat.ofNat (n + 1)) (n + 1)

instance Mathlib.Tactic.Ring.instCSLiftValPNatNatToPNat {n : ℕ} {h : 0 < n} : CSLiftVal (n.toPNat h) n

instance Mathlib.Tactic.Ring.instCSLiftValPNatNatSuccPNatHAddOfNat {n : ℕ} : CSLiftVal n.succPNat (n + 1)

instance Mathlib.Tactic.Ring.instCSLiftValPNatNatToPNat'HAddPredOfNat {n : ℕ} : CSLiftVal n.toPNat' (n.pred + 1)

instance Mathlib.Tactic.Ring.instCSLiftValPNatNatDivExactHAddDivOfNat {n k : ℕ+} : CSLiftVal (n.divExact k) (n.div k + 1)

instance Mathlib.Tactic.Ring.instCSLiftValPNatNatHAdd {n : ℕ+} {n' : ℕ} {k : ℕ+} {k' : ℕ} [h1 : CSLiftVal n n'] [h2 : CSLiftVal k k'] : CSLiftVal (n + k) (n' + k')

instance Mathlib.Tactic.Ring.instCSLiftValPNatNatHMul {n : ℕ+} {n' : ℕ} {k : ℕ+} {k' : ℕ} [h1 : CSLiftVal n n'] [h2 : CSLiftVal k k'] : CSLiftVal (n * k) (n' * k')

instance Mathlib.Tactic.Ring.instCSLiftValPNatNatHPow {n : ℕ+} {n' k : ℕ} [h1 : CSLiftVal n n'] : CSLiftVal (n ^ k) (n' ^ k)