Real

📁 Source: Mathlib/Topology/Algebra/Star/Real.lean

Statistics

Metric	Count
Definitions	0
Theorems instContinuousStar, instContinuousStarReal	2
Total	2

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instContinuousStar 📖	mathematical	—	ContinuousStar NNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal StarRing.toStarAddMonoid instStarRingNNReal	—	continuous_id

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instContinuousStarReal 📖	mathematical	—	ContinuousStar Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.commRing StarRing.toStarAddMonoid instStarRingReal	—	continuous_id

---

← Back to Index