Theorems · Theorem · real analysis
Real.mul_self_sqrt
∀ {x : ℝ}, 0 ≤ x → √x * √x = x- Defined in
- Mathlib.Analysis.Real.Sqrt
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 127 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 · cited by 545
- Real.toNNRealproof · cited by 267
- NNReal.sqrtproof · cited by 91
- Real.coe_toNNRealproof · cited by 27
- NNReal.coe_mulproof · cited by 13
- NNReal.mul_self_sqrtproof · cited by 3
Cited by23
Results whose statement or proof uses this declaration.
- Real.sq_sqrtproof · cited by 53
- Real.sqrt_eq_rpowproof · cited by 25
- Complex.normSq_eq_norm_sqproof · cited by 14
- Real.sqrt_mul_selfproof · cited by 14
- Complex.norm_mul_self_eq_normSqproof · cited by 5
- irrational_sqrt_ratCast_iff_of_nonnegproof · cited by 3
- Real.sqrt_eq_iff_mul_self_eqproof · cited by 3
- CFC.sqrt_eq_real_sqrtproof · cited by 2
- EuclideanGeometry.Sphere.dist_div_cos_oangle_center_div_two_eq_radiusproof · cited by 2
- abs_integral_sub_setIntegral_mulExpNegMulSq_comp_ltproof · cited by 1
- UpperHalfPlane.isElliptic_of_exists_smul_eq_selfproof · cited by 1
- EuclideanGeometry.existsUnique_dist_eq_of_insertproof · cited by 1