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.instCSLiftValPNatNatInstCSLiftPNatNatOfNatHAddInstHAddInstAddNatInstOfNatNatInstOfNatPNatHAddNatInstHAddInstAddNatOfNat {n : ℕ} : Mathlib.Tactic.Ring.CSLiftVal (OfNat.ofNat (n + 1)) (n + 1)

Equations

• (_ : Mathlib.Tactic.Ring.CSLiftVal (OfNat.ofNat (n + 1)) (n + 1)) = (_ : Mathlib.Tactic.Ring.CSLiftVal (OfNat.ofNat (n + 1)) (n + 1))

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

Equations

• (_ : Mathlib.Tactic.Ring.CSLiftVal (Nat.toPNat n) n) = (_ : Mathlib.Tactic.Ring.CSLiftVal (Nat.toPNat n) n)

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

Equations

• (_ : Mathlib.Tactic.Ring.CSLiftVal (Nat.succPNat n) (n + 1)) = (_ : Mathlib.Tactic.Ring.CSLiftVal (Nat.succPNat n) (n + 1))

instance Mathlib.Tactic.Ring.instCSLiftValPNatNatInstCSLiftPNatNatToPNat'HAddInstHAddInstAddNatPredOfNat {n : ℕ} : Mathlib.Tactic.Ring.CSLiftVal (Nat.toPNat' n) (Nat.pred n + 1)

Equations

• (_ : Mathlib.Tactic.Ring.CSLiftVal (Nat.toPNat' n) (Nat.pred n + 1)) = (_ : Mathlib.Tactic.Ring.CSLiftVal (Nat.toPNat' n) (Nat.pred n + 1))

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

Equations

• (_ : Mathlib.Tactic.Ring.CSLiftVal (PNat.divExact n k) (PNat.div n k + 1)) = (_ : Mathlib.Tactic.Ring.CSLiftVal (PNat.divExact n k) (PNat.div n k + 1))

instance Mathlib.Tactic.Ring.instCSLiftValPNatNatInstCSLiftPNatNatHAddInstHAddInstPNatAddInstAddNat {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

• (_ : Mathlib.Tactic.Ring.CSLiftVal (n + k) (n' + k')) = (_ : Mathlib.Tactic.Ring.CSLiftVal (n + k) (n' + k'))

instance Mathlib.Tactic.Ring.instCSLiftValPNatNatInstCSLiftPNatNatHMulInstHMulInstPNatMulInstMulNat {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

• (_ : Mathlib.Tactic.Ring.CSLiftVal (n * k) (n' * k')) = (_ : Mathlib.Tactic.Ring.CSLiftVal (n * k) (n' * k'))

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

Equations

• (_ : Mathlib.Tactic.Ring.CSLiftVal (n ^ k) (n' ^ k)) = (_ : Mathlib.Tactic.Ring.CSLiftVal (n ^ k) (n' ^ k))