Rat

📁 Source: Mathlib/Analysis/Normed/Group/Rat.lean

Statistics

Metric	Count
Definitions instNormedAddCommGroup	1
Theorems norm_cast_rat, norm_cast_real	2
Total	3

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_cast_rat 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm Rat.instNormedAddCommGroup instNormedAddCommGroup	—	Rat.norm_cast_real norm_cast_real

Rat

Definitions

Name	Category	Theorems
instNormedAddCommGroup 📖	CompOp	3 math math: norm_cast_real, Int.norm_cast_rat, instHasSolidNormRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_cast_real 📖	mathematical	—	Norm.norm Real Real.norm Real.instRatCast NormedAddCommGroup.toNorm instNormedAddCommGroup	—	—

---

← Back to Index