Theorems · Definition · complex analysis
RCLike.sqrt
{𝕜 : Type u_1} → [RCLike 𝕜] → 𝕜 → 𝕜The square root on RCLike.
- Defined in
- Mathlib.Analysis.RCLike.Sqrt
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- RCLike
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Complexproof · cited by 5,565
- RCLikestatement and proof · cited by 2,829
- Complex.sqrtproof · cited by 32
- RCLike.mapproof · cited by 14
Cited by15
Results whose statement or proof uses this declaration.
- RCLike.sqrt_eq_itestatement · cited by 4
- RCLike.sqrt_neg_of_nonnegstatement and proof · cited by 1
- RCLike.sqrt_of_nonnegstatement · cited by 1
- RCLike.sqrt_onestatement · cited by 1
- RCLike.re_sqrt_ofRealstatement · cited by 1
- RCLike.sqrt_eq_real_add_itestatement · cited by 0
- RCLike.sqrt_mapstatement · cited by 0
- RCLike.sqrt_neg_Istatement · cited by 0
- RCLike.sqrt_neg_onestatement · cited by 0
- RCLike.sqrt_realstatement and proof · cited by 0
- RCLike.sqrt_zerostatement · cited by 0
- Matrix.PosSemidef.det_sqrtstatement and proof · cited by 0