Ultra

📁 Source: Mathlib/Analysis/Normed/Order/Hom/Ultra.lean

Statistics

Metric	Count
Definitions	0
Theorems isUltrametricDist	1
Total	1

AddGroupSeminormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUltrametricDist 📖	mathematical	IsNonarchimedean Real Real.linearOrder AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DFunLike.coe Dist PseudoMetricSpace.toDist SeminormedAddGroup.toPseudoMetricSpace toSeminormedAddGroup	IsUltrametricDist	—	dist_eq_norm sub_add_sub_cancel

---

← Back to Index