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, sqrt_eq_exp	24
Total	24

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 DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid 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 Complex 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 instReflLe 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 instReflLe 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 instReflLe 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 DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField 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 NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing 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 DenselyNormedField.toNormedField toDenselyNormedField 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

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sqrt_eq_exp 📖	mathematical	—	Complex.sqrt Complex.exp Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.log instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat div_eq_mul_inv

---

← Back to Index