Continuous functions as a star-ordered ring

theorem ContinuousMap.starOrderedRing_of_sqrt {α : Type u_1} [TopologicalSpace α] {R : Type u_2} [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [TopologicalSpace R] [ContinuousStar R] [TopologicalRing R] (sqrt : R → R) (h_continuousOn : ContinuousOn sqrt {x : R | 0 ≤ x}) (h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x) : StarOrderedRing C(α, R)

instance ContinuousMap.instStarOrderedRingRCLike {α : Type u_1} [TopologicalSpace α] {𝕜 : Type u_2} [RCLike 𝕜] : StarOrderedRing C(α, 𝕜)

Equations

• ⋯ = ⋯

instance ContinuousMap.instStarOrderedRingReal {α : Type u_1} [TopologicalSpace α] : StarOrderedRing C(α, ℝ)

Equations

• ⋯ = ⋯

instance ContinuousMap.instStarOrderedRingComplex {α : Type u_1} [TopologicalSpace α] : StarOrderedRing C(α, ℂ)

Equations

• ⋯ = ⋯

instance ContinuousMap.instStarOrderedRingNNReal {α : Type u_1} [TopologicalSpace α] : StarOrderedRing C(α, NNReal)

Equations

• ⋯ = ⋯