Documentation Verification Report

Hyperoperation

📁 Source: Mathlib/Data/Nat/Hyperoperation.lean

Statistics

Metric	Count
Definitions `hyperoperation`	1
Theorems `hyperoperation_ge_four_zero`, `hyperoperation_ge_three_eq_one`, `hyperoperation_ge_three_one`, `hyperoperation_ge_two_eq_self`, `hyperoperation_one`, `hyperoperation_recursion`, `hyperoperation_three`, `hyperoperation_two`, `hyperoperation_two_two_eq_four`, `hyperoperation_zero`	10
Total	11

(root)

Definitions

Name	Category	Theorems
`hyperoperation` 📖	CompOp	10 math math: `hyperoperation_ge_four_zero`, `hyperoperation_ge_three_eq_one`, `hyperoperation_two_two_eq_four`, `hyperoperation_two`, `hyperoperation_ge_three_one`, `hyperoperation_recursion`, `hyperoperation_three`, `hyperoperation_one`, `hyperoperation_ge_two_eq_self`, `hyperoperation_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hyperoperation_ge_four_zero` 📖	mathematical	—	`hyperoperation` `Even` `Nat.instDecidablePredEven`	—	—
`hyperoperation_ge_three_eq_one` 📖	mathematical	—	`hyperoperation`	—	—
`hyperoperation_ge_three_one` 📖	mathematical	—	`hyperoperation`	—	—
`hyperoperation_ge_two_eq_self` 📖	mathematical	—	`hyperoperation`	—	—
`hyperoperation_one` 📖	mathematical	—	`hyperoperation`	—	—
`hyperoperation_recursion` 📖	mathematical	—	`hyperoperation`	—	—
`hyperoperation_three` 📖	mathematical	—	`hyperoperation` `Monoid.toNatPow` `Nat.instMonoid`	—	—
`hyperoperation_two` 📖	mathematical	—	`hyperoperation`	—	—
`hyperoperation_two_two_eq_four` 📖	mathematical	—	`hyperoperation`	—	—
`hyperoperation_zero` 📖	mathematical	—	`hyperoperation`	—	—

---

← Back to Index