Documentation Verification Report

ULift

📁 Source: Mathlib/Algebra/Field/ULift.lean

Statistics

Metric	Count
Definitions `divisionRing`, `divisionSemiring`, `instNNRatCast`, `instRatCast`, `semifield`	5
Theorems `down_nnratCast`, `down_ratCast`, `up_nnratCast`, `up_ratCast`	4
Total	9

ULift

Definitions

Name	Category	Theorems
`divisionRing` 📖	CompOp	—
`divisionSemiring` 📖	CompOp	—
`instNNRatCast` 📖	CompOp	2 math math: `down_nnratCast`, `up_nnratCast`
`instRatCast` 📖	CompOp	2 math math: `up_ratCast`, `down_ratCast`
`semifield` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`down_nnratCast` 📖	mathematical	—	`NNRat.cast` `instNNRatCast`	—	—
`down_ratCast` 📖	mathematical	—	`instRatCast`	—	—
`up_nnratCast` 📖	mathematical	—	`NNRat.cast` `instNNRatCast`	—	—
`up_ratCast` 📖	mathematical	—	`instRatCast`	—	—

---

← Back to Index