Documentation Verification Report

PNat

📁 Source: Mathlib/Tactic/Ring/PNat.lean

Statistics

Metric	Count
Definitions `instCSLiftPNatNat`	1
Theorems `instCSLiftValPNatNatDivExactHAddDivOfNat`, `instCSLiftValPNatNatHAdd`, `instCSLiftValPNatNatHMul`, `instCSLiftValPNatNatHPow`, `instCSLiftValPNatNatOfNatHAdd`, `instCSLiftValPNatNatSuccPNatHAddOfNat`, `instCSLiftValPNatNatToPNat`, `instCSLiftValPNatNatToPNat'HAddPredOfNat`	8
Total	9

Mathlib.Tactic.Ring

Definitions

Name	Category	Theorems
`instCSLiftPNatNat` 📖	CompOp	8 math math: `instCSLiftValPNatNatToPNat`, `instCSLiftValPNatNatHMul`, `instCSLiftValPNatNatDivExactHAddDivOfNat`, `instCSLiftValPNatNatOfNatHAdd`, `instCSLiftValPNatNatSuccPNatHAddOfNat`, `instCSLiftValPNatNatHAdd`, `instCSLiftValPNatNatHPow`, `instCSLiftValPNatNatToPNat'HAddPredOfNat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCSLiftValPNatNatDivExactHAddDivOfNat` 📖	mathematical	—	`CSLiftVal` `PNat` `instCSLiftPNatNat` `PNat.divExact` `PNat.div`	—	—
`instCSLiftValPNatNatHAdd` 📖	mathematical	—	`CSLiftVal` `PNat` `instCSLiftPNatNat` `instAddPNat`	—	`CSLiftVal.eq`
`instCSLiftValPNatNatHMul` 📖	mathematical	—	`CSLiftVal` `PNat` `instCSLiftPNatNat` `instMulPNat`	—	`CSLiftVal.eq`
`instCSLiftValPNatNatHPow` 📖	mathematical	—	`CSLiftVal` `PNat` `instCSLiftPNatNat` `Monoid.toNatPow` `CommMonoid.toMonoid` `PNat.instCommMonoid` `Nat.instMonoid`	—	`CSLiftVal.eq`
`instCSLiftValPNatNatOfNatHAdd` 📖	mathematical	—	`CSLiftVal` `PNat` `instCSLiftPNatNat`	—	—
`instCSLiftValPNatNatSuccPNatHAddOfNat` 📖	mathematical	—	`CSLiftVal` `PNat` `instCSLiftPNatNat` `Nat.succPNat`	—	—
`instCSLiftValPNatNatToPNat` 📖	mathematical	—	`CSLiftVal` `PNat` `instCSLiftPNatNat` `Nat.toPNat`	—	—
`instCSLiftValPNatNatToPNat'HAddPredOfNat` 📖	mathematical	—	`CSLiftVal` `PNat` `instCSLiftPNatNat` `Nat.toPNat'`	—	—

---

← Back to Index