noncomputable def PReal.sqrt (x : ℝ>0) : ℝ>0

Equations

• x.sqrt = ⟨√↑x, ⋯⟩

@[simp]

theorem PReal.sqrt_to_real (x : ℝ>0) : ↑x.sqrt = √↑x

@[simp]

theorem PReal.mul_self_sqrt (x : ℝ>0) : x.sqrt * x.sqrt = x