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 100]

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

• ⋯ = ⋯

instance ContinuousMapZero.instStarOrderedRing {α : Type u_1} [TopologicalSpace α] [Zero α] {R : Type u_2} [TopologicalSpace R] [OrderedCommSemiring R] [NoZeroDivisors R] [StarRing R] [StarOrderedRing R] [TopologicalSemiring R] [ContinuousStar R] [StarOrderedRing C(α, R)] : StarOrderedRing (ContinuousMapZero α R)

Equations

• ⋯ = ⋯

instance ContinuousMapZero.instStarOrderedRingReal {α : Type u_1} [TopologicalSpace α] [Zero α] : StarOrderedRing (ContinuousMapZero α ℝ)

Equations

• ⋯ = ⋯

instance ContinuousMapZero.instStarOrderedRingComplex {α : Type u_1} [TopologicalSpace α] [Zero α] : StarOrderedRing (ContinuousMapZero α ℂ)

Equations

• ⋯ = ⋯

instance ContinuousMapZero.instStarOrderedRingNNReal {α : Type u_1} [TopologicalSpace α] [Zero α] : StarOrderedRing (ContinuousMapZero α NNReal)

Equations

• ⋯ = ⋯