Theorems · Theorem · real analysis
Real.sqrt_inv
∀ (x : ℝ), √x⁻¹ = (√x)⁻¹
- Defined in
- Mathlib.Analysis.Real.Sqrt
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Realstatement and proof · cited by 25,697
- NNRealproof · cited by 4,310
- NNReal.toRealproof · cited by 1,260
- Real.sqrtstatement and proof · cited by 545
- Real.toNNRealproof · cited by 267
- NNReal.sqrtproof · cited by 91
- NNReal.coe_invproof · cited by 11
- Real.toNNReal_invproof · cited by 5
- NNReal.sqrt_invproof · cited by 1
Cited by13
Results whose statement or proof uses this declaration.
- Real.sqrt_divproof · cited by 4
- Polynomial.Chebyshev.integral_measureT_eq_integral_cosproof · cited by 3
- Real.sqrt_div'proof · cited by 3
- Real.inv_sqrt_one_add_tan_sqproof · cited by 2
- Polynomial.Chebyshev.integrable_measureTproof · cited by 2
- ProbabilityTheory.lintegral_gaussianPDFReal_eq_oneproof · cited by 2
- Polynomial.Chebyshev.intervalIntegrable_sqrt_one_sub_sq_invproof · cited by 1
- Complex.sqrt_Iproof · cited by 1
- Polynomial.Chebyshev.integral_measureTproof · cited by 1
- Complex.sqrt_neg_Iproof · cited by 1
- RCLike.sqrt_neg_Iproof · cited by 0
- Real.arctan_eq_arccosproof · cited by 0