Ultra

Statistics

Metric	Count
Definitions	0
Theorems `normedAlgebra_iff`, `of_normedAlgebra`, `of_normedAlgebra'`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`normedAlgebra_iff` 📖	mathematical	—	`IsUltrametricDist` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	—	`of_normedAlgebra'` `NormedDivisionRing.to_normOneClass` `of_normedAlgebra`
`of_normedAlgebra` 📖	mathematical	—	`IsUltrametricDist` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing`	—	`isUltrametricDist_iff_forall_norm_natCast_le_one` `norm_algebraMap'` `NormedDivisionRing.to_normOneClass` `algebraMap.coe_natCast`
`of_normedAlgebra'` 📖	mathematical	—	`IsUltrametricDist` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	—	`dist_algebraMap'` `dist_triangle_max`

---