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 : Mathlib.Tactic.Ring.CSLift ℕ+ ℕ

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯