Documentation Verification Report

HurwitzRatHat

📁 Source: FLT/Data/HurwitzRatHat.lean

Statistics

Metric	Count
Definitions `HurwitzHat`, `instRing`, `«term𝓞^»`, `HurwitzRat`, `instRing`, `termD`, `HurwitzRatHat`, `instRing`, `j₁`, `j₂`, `«termD^»`	11
Theorems `canonicalForm`, `completed_units`, `injective_hRat`, `injective_zHat`	4
Total	15
⚠️ With sorry `canonicalForm`, `completed_units`, `injective_hRat`, `injective_zHat`	4

HurwitzHat

Definitions

Name	Category	Theorems
`instRing` 📖	CompOp	3 math math: `HurwitzRatHat.canonicalForm`, `HurwitzRatHat.injective_zHat`, `HurwitzRatHat.completed_units`
`«term𝓞^»` 📖	CompOp	—

HurwitzRat

Definitions

Name	Category	Theorems
`instRing` 📖	CompOp	3 math math: `HurwitzRatHat.injective_hRat`, `HurwitzRatHat.canonicalForm`, `HurwitzRatHat.completed_units`
`termD` 📖	CompOp	—

HurwitzRatHat

Definitions

Name	Category	Theorems
`instRing` 📖	CompOp	4 math math: `injective_hRat`, `canonicalForm`, `injective_zHat`, `completed_units`
`j₁` 📖	CompOp	3 math math: `injective_hRat`, `canonicalForm`, `completed_units`
`j₂` 📖	CompOp	3 math math: `canonicalForm`, `injective_zHat`, `completed_units`
`«termD^»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`canonicalForm` 📖 ⚠️	mathematical	—	`HurwitzRatHat` `instRing` `HurwitzRat` `HurwitzRat.instRing` `j₁` `Hurwitz` `Hurwitz.ring` `Hurwitz.instOne` `HurwitzHat` `HurwitzHat.instRing` `j₂`	—	—
`completed_units` 📖 ⚠️	mathematical	—	`HurwitzRatHat` `instRing` `HurwitzRat` `HurwitzRat.instRing` `j₁` `HurwitzHat` `HurwitzHat.instRing` `j₂`	—	—
`injective_hRat` 📖 ⚠️	mathematical	—	`HurwitzRat` `HurwitzRatHat` `HurwitzRat.instRing` `instRing` `j₁`	—	—
`injective_zHat` 📖 ⚠️	mathematical	—	`HurwitzHat` `HurwitzRatHat` `HurwitzHat.instRing` `instRing` `j₂`	—	—

(root)

Definitions

Name	Category	Theorems
`HurwitzHat` 📖	CompOp	3 math math: `HurwitzRatHat.canonicalForm`, `HurwitzRatHat.injective_zHat`, `HurwitzRatHat.completed_units`
`HurwitzRat` 📖	CompOp	3 math math: `HurwitzRatHat.injective_hRat`, `HurwitzRatHat.canonicalForm`, `HurwitzRatHat.completed_units`
`HurwitzRatHat` 📖	CompOp	4 math math: `HurwitzRatHat.injective_hRat`, `HurwitzRatHat.canonicalForm`, `HurwitzRatHat.injective_zHat`, `HurwitzRatHat.completed_units`

---

← Back to Index