Documentation Verification Report

PNatPowAssoc

📁 Source: Mathlib/Algebra/Group/PNatPowAssoc.lean

Statistics

Metric	Count
Definitions `PNatPowAssoc`	1
Theorems `ppow_add`, `ppow_one`, `instPNatPowAssoc`, `instPNatPowAssoc`, `ppow_add`, `ppow_eq_pow`, `ppow_mul`, `ppow_mul'`, `ppow_mul_assoc`, `ppow_mul_comm`, `ppow_one`	11
Total	12

PNatPowAssoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ppow_add` 📖	mathematical	—	`PNat` `instAddPNat`	—	—
`ppow_one` 📖	mathematical	—	`PNat` `instOfNatPNatOfNeZeroNat`	—	—

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instPNatPowAssoc` 📖	mathematical	`PNatPowAssoc`	`instMul` `instPow` `PNat`	—	`ppow_add` `ppow_one`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instPNatPowAssoc` 📖	mathematical	—	`PNatPowAssoc` `instMul` `instPow` `PNat`	—	`ppow_add` `ppow_one`

(root)

Definitions

Name	Category	Theorems
`PNatPowAssoc` 📖	CompData	2 math math: `Prod.instPNatPowAssoc`, `Complex.UnitDisc.instPNatPowAssoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ppow_add` 📖	mathematical	—	`PNat` `instAddPNat`	—	`PNatPowAssoc.ppow_add`
`ppow_eq_pow` 📖	mathematical	—	`PNat` `Monoid.toNatPow` `PNat.val`	—	`ppow_one` `PNat.one_coe` `pow_one` `ppow_add` `PNat.add_coe` `pow_add`
`ppow_mul` 📖	mathematical	—	`PNat` `instMulPNat`	—	`ppow_one` `mul_one` `ppow_add` `mul_add` `Distrib.leftDistribClass`
`ppow_mul'` 📖	mathematical	—	`PNat` `instMulPNat`	—	`mul_comm` `ppow_mul`
`ppow_mul_assoc` 📖	mathematical	—	`PNat`	—	`add_assoc`
`ppow_mul_comm` 📖	mathematical	—	`PNat`	—	`add_comm`
`ppow_one` 📖	mathematical	—	`PNat` `instOfNatPNatOfNeZeroNat`	—	`PNatPowAssoc.ppow_one`

---

← Back to Index