WithTop

📁 Source: Mathlib/Data/Nat/Cast/WithTop.lean

Statistics

Metric	Count
Definitions instWellFoundedRelationWithTopNat	1
Theorems cast_withBot, cast_withTop	2
Total	3

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_withBot 📖	mathematical	—	WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne instAddMonoidWithOne WithBot.some	—	—
cast_withTop 📖	mathematical	—	WithTop AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne instAddMonoidWithOne WithTop.some	—	—

(root)

Definitions

Name	Category	Theorems
instWellFoundedRelationWithTopNat 📖	CompOp	—

---

← Back to Index