Documentation Verification Report

Sqrt

📁 Source: Mathlib/Analysis/RCLike/Sqrt.lean

Statistics

Metric	Count
Definitions	0
Theorems `re_sqrt_ofReal`, `sqrt_I`, `sqrt_eq_real_add_ite`, `sqrt_map`, `sqrt_neg_I`, `sqrt_neg_of_nonneg`, `sqrt_neg_one`, `sqrt_of_nonneg`, `sqrt_one`, `sqrt_zero`, `re_sqrt_ofReal`, `sqrt_I`, `sqrt_complex`, `sqrt_eq_ite`, `sqrt_eq_real_add_ite`, `sqrt_map`, `sqrt_neg_I`, `sqrt_neg_of_nonneg`, `sqrt_neg_one`, `sqrt_of_nonneg`, `sqrt_one`, `sqrt_real`, `sqrt_zero`	23
Total	23

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`re_sqrt_ofReal` 📖	mathematical	—	`re` `sqrt` `ofReal` `Real.sqrt`	—	`Nat.instAtLeastTwoHAddOfNat` `cpow_inv_two_re` `norm_real`
`sqrt_I` 📖	mathematical	—	`sqrt` `I` `Complex` `instMul` `ofReal` `Real.sqrt` `Real` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `instAdd` `instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `sqrt.eq_1` `re_add_im` `cpow_inv_two_im_eq_sqrt` `Real.instZeroLEOneClass` `cpow_inv_two_re` `norm_I` `add_zero` `one_div` `Real.sqrt_inv` `ofReal_inv` `sub_zero` `mul_add` `Distrib.leftDistribClass` `mul_one`
`sqrt_eq_real_add_ite` 📖	mathematical	—	`sqrt` `Complex` `instAdd` `ofReal` `Real.sqrt` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instAdd` `Norm.norm` `instNorm` `re` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `instMul` `Real.instLE` `Real.instZero` `im` `Real.decidableLE` `instOne` `instNeg` `Real.instSub` `I`	—	`Nat.instAtLeastTwoHAddOfNat` `cpow_inv_two_re` `sqrt.eq_1` `cpow_inv_two_im_eq_sqrt` `one_mul` `re_add_im` `LT.lt.not_ge` `neg_one_mul` `cpow_inv_two_im_eq_neg_sqrt`
`sqrt_map` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `Real` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.im` `RCLike.I` `Real.instOne`	`sqrt` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Complex` `instRCLike` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedAlgebra.toNormedSpace` `RCLike.toNormedAlgebra` `ContinuousLinearMap.funLike` `RCLike.map` `RCLike.sqrt`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `RCLike.ofReal_re` `RCLike.mul_re` `RCLike.I_re` `MulZeroClass.mul_zero` `RCLike.ofReal_im` `mul_one` `sub_self` `add_zero` `RCLike.mul_im` `zero_add` `re_add_im`
`sqrt_neg_I` 📖	mathematical	—	`sqrt` `Complex` `instNeg` `I` `instMul` `ofReal` `Real.sqrt` `Real` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `instSub` `instOne`	—	`Nat.instAtLeastTwoHAddOfNat` `sqrt.eq_1` `re_add_im` `cpow_inv_two_im_eq_neg_sqrt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `cpow_inv_two_re` `norm_neg` `norm_I` `neg_zero` `add_zero` `one_div` `Real.sqrt_inv` `ofReal_inv` `sub_zero` `ofReal_neg` `neg_mul` `mul_sub` `mul_one`
`sqrt_neg_of_nonneg` 📖	mathematical	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instZero`	`sqrt` `instNeg` `instMul` `I`	—	`RCLike.nonneg_iff_exists_ofReal` `sqrt_of_nonneg` `re_add_im` `Nat.instAtLeastTwoHAddOfNat` `cpow_inv_two_re` `norm_neg` `norm_real` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_neg_cancel` `zero_div` `Real.sqrt_zero` `cpow_inv_two_im_eq_sqrt` `neg_zero` `sub_neg_eq_add` `add_self_div_two` `CharZero.NeZero.two` `RCLike.charZero_rclike` `mul_comm` `zero_add`
`sqrt_neg_one` 📖	mathematical	—	`sqrt` `Complex` `instNeg` `instOne` `I`	—	`sqrt_neg_of_nonneg` `RCLike.toZeroLEOneClass` `sqrt_one` `mul_one`
`sqrt_of_nonneg` 📖	mathematical	`Complex` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `instZero`	`sqrt` `ofReal` `Real.sqrt` `re`	—	`RCLike.nonneg_iff_exists_ofReal` `re_add_im` `re_sqrt_ofReal` `Nat.instAtLeastTwoHAddOfNat` `cpow_inv_two_im_eq_sqrt` `norm_real` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_self` `zero_div` `Real.sqrt_zero` `MulZeroClass.zero_mul` `add_zero`
`sqrt_one` 📖	mathematical	—	`sqrt` `Complex` `instOne`	—	`one_cpow`
`sqrt_zero` 📖	mathematical	—	`sqrt` `Complex` `instZero`	—	`zero_cpow` `instCharZero`

RCLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`re_sqrt_ofReal` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Real` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `re` `sqrt` `ofReal` `Real.sqrt`	—	`ofReal_re` `ofReal_im` `MulZeroClass.zero_mul` `add_zero` `Complex.re_sqrt_ofReal` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `mul_re` `I_re` `MulZeroClass.mul_zero` `sub_self`
`sqrt_I` 📖	mathematical	—	`sqrt` `I` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `toDenselyNormedField` `ofReal` `Real.sqrt` `Real` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`Nat.instAtLeastTwoHAddOfNat` `sqrt_eq_ite` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.instRingEquivClass` `I_re` `one_mul` `add_comm` `add_zero` `Complex.sqrt_I` `Real.sqrt_inv` `Complex.ofReal_inv` `mul_add` `Distrib.leftDistribClass` `mul_one` `map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `RingEquivClass.toRingHomClass` `ofReal_re` `ofReal_im` `MulZeroClass.zero_mul` `zero_add` `map_sub` `AddMonoidHom.instAddMonoidHomClass` `one_re` `sub_zero` `one_im` `zero_sub` `Complex.ofReal_neg` `neg_mul` `mul_neg` `add_mul` `Distrib.rightDistribClass` `mul_assoc` `Complex.I_mul_I` `neg_neg`
`sqrt_complex` 📖	mathematical	—	`sqrt` `Complex` `Complex.instRCLike` `Complex.sqrt`	—	`map_same_eq_id`
`sqrt_eq_ite` 📖	mathematical	—	`sqrt` `Real` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `im` `I` `Real.instOne` `Real.decidableEq` `RingEquiv` `Complex` `Complex.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Complex.instAdd` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `complexRingEquiv` `Complex.sqrt` `ofReal` `Real.sqrt` `re`	—	`sqrt.eq_1` `Nat.instAtLeastTwoHAddOfNat` `im_eq_zero` `Complex.cpow_inv_two_re` `MulZeroClass.mul_zero` `add_zero` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `MulZeroClass.zero_mul` `Complex.norm_real` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_div_cancel_left₀` `GroupWithZero.toMulDivCancelClass` `charZero_rclike` `abs_of_nonpos` `LT.lt.le` `neg_add_cancel` `zero_div` `Real.sqrt_zero`
`sqrt_eq_real_add_ite` 📖	mathematical	—	`sqrt` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `toDenselyNormedField` `ofReal` `Real.sqrt` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instAdd` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `re` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Distrib.toMul` `Real.instLE` `Real.instZero` `im` `Real.decidableLE` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `Real.instSub` `I`	—	`Nat.instAtLeastTwoHAddOfNat` `sqrt.eq_1` `Complex.sqrt_eq_real_add_ite` `I_eq_zero_or_im_I_eq_one` `re_add_im` `im_eq_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MulZeroClass.mul_zero` `add_zero` `ofReal_re` `MulZeroClass.zero_mul` `Complex.norm_real` `Real.sqrt_div'` `Real.instIsOrderedRing` `Complex.ofReal_div` `one_mul` `Complex.div_ofReal_re` `Complex.div_ofReal_im` `zero_div` `mul_one` `sub_self` `map_div₀` `zero_add` `norm_algebraMap'` `NormedDivisionRing.to_normOneClass` `norm_to_complex` `ite_mul` `neg_mul` `map_add` `SemilinearMapClass.toAddHomClass` `charZero_rclike` `RingHomClass.toLinearMapClassNNRat` `neg_zero` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass`
`sqrt_map` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `Real` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `toDenselyNormedField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `im` `I`	`sqrt` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedAlgebra.toNormedSpace` `toNormedAlgebra` `ContinuousLinearMap.funLike` `map`	—	`I_eq_zero_or_im_I_eq_one` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `ofReal_re` `mul_re` `I_re` `MulZeroClass.mul_zero` `ofReal_im` `MulZeroClass.zero_mul` `sub_self` `add_zero` `mul_im` `zero_add` `Complex.ofReal_mul` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `im_eq_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `NeZero.charZero_one` `charZero_rclike` `mul_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass`
`sqrt_neg_I` 📖	mathematical	—	`sqrt` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `toDenselyNormedField` `I` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `ofReal` `Real.sqrt` `Real` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`Nat.instAtLeastTwoHAddOfNat` `sqrt_eq_ite` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.instRingEquivClass` `map_neg` `AddMonoidHom.instAddMonoidHomClass` `I_re` `neg_zero` `Complex.ofReal_neg` `neg_mul` `one_mul` `add_comm` `add_zero` `Complex.sqrt_neg_I` `Real.sqrt_inv` `Complex.ofReal_inv` `mul_sub` `mul_one` `map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `RingEquivClass.toRingHomClass` `ofReal_re` `ofReal_im` `MulZeroClass.zero_mul` `zero_add` `map_add` `AddMonoidHomClass.toAddHomClass` `one_re` `one_im` `mul_add` `Distrib.leftDistribClass` `mul_neg` `add_mul` `Distrib.rightDistribClass` `mul_assoc` `mul_comm` `Complex.I_mul_I` `neg_sub`
`sqrt_neg_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `toPartialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `toDenselyNormedField`	`sqrt` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `I`	—	`I_eq_zero_or_im_I_eq_one` `sqrt_eq_ite` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `NeZero.charZero_one` `charZero_rclike` `map_neg` `MulZeroClass.zero_mul` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `nonneg_iff` `RingEquiv.symm_apply_eq` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `Complex.instCharZero` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomClass.toLinearMapClassNNRat` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `Complex.sqrt_neg_of_nonneg` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingEquivClass.toNonUnitalRingHomClass` `I_re` `one_mul` `zero_add` `map_add` `AddMonoidHomClass.toAddHomClass` `ofReal_re` `mul_re` `MulZeroClass.mul_zero` `ofReal_im` `mul_one` `sub_self` `add_zero` `mul_im` `Complex.re_add_im`
`sqrt_neg_one` 📖	mathematical	—	`sqrt` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `toDenselyNormedField` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `I`	—	`sqrt_neg_of_nonneg` `toZeroLEOneClass` `sqrt_one` `mul_one`
`sqrt_of_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `toPartialOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `toDenselyNormedField`	`sqrt` `ofReal` `Real.sqrt` `DFunLike.coe` `AddMonoidHom` `Real` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `NormedField.toField` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `re`	—	`I_eq_zero_or_im_I_eq_one` `sqrt_eq_ite` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `NeZero.charZero_one` `charZero_rclike` `RingEquiv.symm_apply_eq` `Complex.sqrt_of_nonneg` `MulZeroClass.mul_zero` `mul_one` `sub_self` `add_zero` `ofReal_re` `ofReal_im` `MulZeroClass.zero_mul`
`sqrt_one` 📖	mathematical	—	`sqrt` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `toDenselyNormedField`	—	`one_re` `one_im` `MulZeroClass.zero_mul` `add_zero` `Complex.sqrt_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass`
`sqrt_real` 📖	mathematical	—	`sqrt` `Real` `Real.instRCLike` `Real.sqrt`	—	`re_sqrt_ofReal`
`sqrt_zero` 📖	mathematical	—	`sqrt` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `toDenselyNormedField`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `MulZeroClass.zero_mul` `add_zero` `Complex.sqrt_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`

---

← Back to Index