Sqrt

📁 Source: Mathlib/Data/Real/Sqrt.lean

Statistics

Metric	Count
Definitions `evalNNRealSqrt`, `evalSqrt`, `sqrtHom`, `«term√_»`	4
Theorems `continuous_sqrt`, `isSquare`, `le_sqrt_iff_sq_le`, `mul_self_sqrt`, `one_le_sqrt`, `sq_sqrt`, `sqrt_div`, `sqrt_eq_iff_eq_sq`, `sqrt_eq_one`, `sqrt_eq_zero`, `sqrt_inv`, `sqrt_le_iff_le_sq`, `sqrt_le_one`, `sqrt_le_sqrt`, `sqrt_lt_sqrt`, `sqrt_mul`, `sqrt_mul_self`, `sqrt_one`, `sqrt_pos`, `sqrt_pos_of_pos`, `sqrt_sq`, `sqrt_zero`, `sum_mul_le_sqrt_mul_sqrt`, `sum_sqrt_mul_sqrt_le`, `abs_le_sqrt`, `coe_sqrt`, `comap_sqrt_atTop`, `continuous_sqrt`, `div_sqrt`, `floor_real_sqrt_eq_nat_sqrt`, `inv_sqrt_two_sub_one`, `isSquare_iff`, `le_sqrt`, `le_sqrt'`, `le_sqrt_of_sq_le`, `lt_sq_of_sqrt_lt`, `lt_sqrt`, `lt_sqrt_of_sq_lt`, `map_sqrt_atTop`, `mul_self_sqrt`, `nat_floor_real_sqrt_eq_nat_sqrt`, `nat_sqrt_le_real_sqrt`, `neg_sqrt_le_of_sq_le`, `neg_sqrt_lt_of_sq_lt`, `one_le_sqrt`, `one_lt_sqrt_two`, `real_sqrt_le_nat_sqrt_succ`, `real_sqrt_lt_nat_sqrt_succ`, `sq_le`, `sq_lt`, `sq_sqrt`, `sq_sqrt'`, `sqrt_div`, `sqrt_div'`, `sqrt_div_self`, `sqrt_div_self'`, `sqrt_eq_cases`, `sqrt_eq_iff_eq_sq`, `sqrt_eq_iff_mul_self_eq`, `sqrt_eq_iff_mul_self_eq_of_pos`, `sqrt_eq_one`, `sqrt_eq_zero`, `sqrt_eq_zero'`, `sqrt_eq_zero_of_nonpos`, `sqrt_inj`, `sqrt_inv`, `sqrt_le_iff`, `sqrt_le_left`, `sqrt_le_one`, `sqrt_le_sqrt`, `sqrt_le_sqrt_iff`, `sqrt_le_sqrt_iff'`, `sqrt_lt`, `sqrt_lt'`, `sqrt_lt_sqrt`, `sqrt_lt_sqrt_iff`, `sqrt_lt_sqrt_iff_of_pos`, `sqrt_monotone`, `sqrt_mul`, `sqrt_mul'`, `sqrt_mul_self`, `sqrt_mul_self_eq_abs`, `sqrt_ne_zero`, `sqrt_ne_zero'`, `sqrt_nonneg`, `sqrt_one`, `sqrt_one_add_le`, `sqrt_pos`, `sqrt_pos_of_pos`, `sqrt_prod`, `sqrt_sq`, `sqrt_sq_eq_abs`, `sqrt_two_lt_three_halves`, `sqrt_zero`, `strictMonoOn_sqrt`, `sum_mul_le_sqrt_mul_sqrt`, `sum_sqrt_mul_sqrt_le`, `tendsto_sqrt_atTop`	98
Total	102

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalNNRealSqrt` 📖	CompOp	—
`evalSqrt` 📖	CompOp	—

NNReal

Definitions

Name	Category	Theorems
`sqrtHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_sqrt` 📖	mathematical	—	`Continuous` `NNReal` `instTopologicalSpace` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt`	—	`OrderIso.continuous` `instOrderTopology`
`isSquare` 📖	mathematical	—	`IsSquare` `NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`mul_self_sqrt`
`le_sqrt_iff_sq_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `sqrt` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal`	—	`OrderIso.to_galoisConnection`
`mul_self_sqrt` 📖	mathematical	—	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt`	—	`sq` `sq_sqrt`
`one_le_sqrt` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `sqrt`	—	`sqrt_one` `sqrt_le_sqrt`
`sq_sqrt` 📖	mathematical	—	`NNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt`	—	`OrderIso.symm_apply_apply`
`sqrt_div` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `instDiv`	—	`map_div₀` `MonoidWithZeroHom.monoidWithZeroHomClass`
`sqrt_eq_iff_eq_sq` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal`	—	`Equiv.apply_eq_iff_eq_symm_apply`
`sqrt_eq_one` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `instOneNNReal`	—	`one_pow`
`sqrt_eq_zero` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `instZeroNNReal`	—	`zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`
`sqrt_inv` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `instInv`	—	`map_inv₀` `MonoidWithZeroHom.monoidWithZeroHomClass`
`sqrt_le_iff_le_sq` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `sqrt` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal`	—	`OrderIso.to_galoisConnection`
`sqrt_le_one` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `sqrt` `instOneNNReal`	—	`sqrt_one` `sqrt_le_sqrt`
`sqrt_le_sqrt` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `sqrt`	—	`OrderIso.le_iff_le`
`sqrt_lt_sqrt` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `DFunLike.coe` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso` `sqrt`	—	`OrderIso.lt_iff_lt`
`sqrt_mul` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`sqrt_eq_iff_eq_sq` `mul_pow` `sq_sqrt`
`sqrt_mul_self` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`sq` `sqrt_sq`
`sqrt_one` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `instOneNNReal`	—	—
`sqrt_pos` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `DFunLike.coe` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso` `sqrt`	—	`instCanonicallyOrderedAdd`
`sqrt_pos_of_pos` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`DFunLike.coe` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso` `sqrt`	—	`sqrt_pos`
`sqrt_sq` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal`	—	`OrderIso.apply_symm_apply`
`sqrt_zero` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `sqrt` `instZeroNNReal`	—	—
`sum_mul_le_sqrt_mul_sqrt` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `sqrt` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`LE.le.trans_eq` `le_sqrt_iff_sq_le` `Finset.sum_mul_sq_le_sq_mul_sq` `instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `sqrt_mul`
`sum_sqrt_mul_sqrt_le` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `sqrt`	—	`Finset.sum_congr` `sq_sqrt` `sum_mul_le_sqrt_mul_sqrt`

Real

Definitions

Name	Category	Theorems
`«term√_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_le_sqrt` 📖	mathematical	`Real` `instLE` `Monoid.toNatPow` `instMonoid`	`abs` `lattice` `instAddGroup` `sqrt`	—	`sqrt_sq_eq_abs` `sqrt_le_sqrt`
`coe_sqrt` 📖	mathematical	—	`NNReal.toReal` `DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `NNReal.sqrt` `sqrt`	—	`sqrt.eq_1` `toNNReal_coe`
`comap_sqrt_atTop` 📖	mathematical	—	`Filter.comap` `Real` `sqrt` `Filter.atTop` `instPreorder`	—	`NNReal.comap_coe_atTop` `OrderIso.comap_atTop` `comap_toNNReal_atTop`
`continuous_sqrt` 📖	mathematical	—	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `sqrt`	—	`Continuous.comp'` `NNReal.continuous_coe` `NNReal.continuous_sqrt` `continuous_real_toNNReal`
`div_sqrt` 📖	mathematical	—	`Real` `DivInvMonoid.toDiv` `instDivInvMonoid` `sqrt`	—	—
`floor_real_sqrt_eq_nat_sqrt` 📖	mathematical	—	`Int.floor` `Real` `instRing` `linearOrder` `instFloorRing` `sqrt` `instNatCast`	—	`Int.floor_eq_iff` `nat_sqrt_le_real_sqrt` `real_sqrt_lt_nat_sqrt_succ`
`inv_sqrt_two_sub_one` 📖	mathematical	—	`Real` `instInv` `instSub` `sqrt` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `instOne` `instAdd`	—	—
`isSquare_iff` 📖	mathematical	—	`IsSquare` `Real` `instMul` `instLE` `instZero`	—	`IsSquare.nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `mul_self_sqrt`
`le_sqrt` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt` `Monoid.toNatPow` `instMonoid`	—	`le_iff_le_iff_lt_iff_lt` `sqrt_lt`
`le_sqrt'` 📖	mathematical	`Real` `instLT` `instZero`	`instLE` `sqrt` `Monoid.toNatPow` `instMonoid`	—	`le_iff_le_iff_lt_iff_lt` `sqrt_lt'`
`le_sqrt_of_sq_le` 📖	mathematical	`Real` `instLE` `Monoid.toNatPow` `instMonoid`	`sqrt`	—	`sq_le` `LE.le.trans` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`lt_sq_of_sqrt_lt` 📖	mathematical	`Real` `instLT` `sqrt`	`Monoid.toNatPow` `instMonoid`	—	`LE.le.trans_lt` `sqrt_nonneg` `sqrt_lt_sqrt_iff_of_pos` `sq_pos_of_pos` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `sqrt_sq` `LT.lt.le`
`lt_sqrt` 📖	mathematical	`Real` `instLE` `instZero`	`instLT` `sqrt` `Monoid.toNatPow` `instMonoid`	—	`sqrt_lt_sqrt_iff` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `sqrt_sq`
`lt_sqrt_of_sq_lt` 📖	mathematical	`Real` `instLT` `Monoid.toNatPow` `instMonoid`	`sqrt`	—	`sq_lt`
`map_sqrt_atTop` 📖	mathematical	—	`Filter.map` `Real` `sqrt` `Filter.atTop` `instPreorder`	—	`map_toNNReal_atTop` `OrderIso.map_atTop` `NNReal.map_coe_atTop`
`mul_self_sqrt` 📖	mathematical	`Real` `instLE` `instZero`	`instMul` `sqrt`	—	`sqrt.eq_1` `NNReal.coe_mul` `NNReal.mul_self_sqrt` `coe_toNNReal`
`nat_floor_real_sqrt_eq_nat_sqrt` 📖	mathematical	—	`Nat.floor` `Real` `semiring` `partialOrder` `FloorRing.toFloorSemiring` `instRing` `linearOrder` `instIsStrictOrderedRing` `instFloorRing` `sqrt` `instNatCast`	—	`instIsStrictOrderedRing` `Nat.floor_eq_iff` `sqrt_nonneg` `nat_sqrt_le_real_sqrt` `real_sqrt_lt_nat_sqrt_succ`
`nat_sqrt_le_real_sqrt` 📖	mathematical	—	`Real` `instLE` `instNatCast` `sqrt`	—	`le_sqrt` `Nat.cast_nonneg` `instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `Nat.sqrt_le'`
`neg_sqrt_le_of_sq_le` 📖	mathematical	`Real` `instLE` `Monoid.toNatPow` `instMonoid`	`instNeg` `sqrt`	—	`sq_le` `LE.le.trans` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`neg_sqrt_lt_of_sq_lt` 📖	mathematical	`Real` `instLT` `Monoid.toNatPow` `instMonoid`	`instNeg` `sqrt`	—	`sq_lt`
`one_le_sqrt` 📖	mathematical	—	`Real` `instLE` `instOne` `sqrt`	—	`sqrt_one` `sqrt_le_sqrt_iff'` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing`
`one_lt_sqrt_two` 📖	mathematical	—	`Real` `instLT` `instOne` `sqrt` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sqrt_one` `sqrt_lt_sqrt` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `instIsOrderedRing` `instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing`
`real_sqrt_le_nat_sqrt_succ` 📖	mathematical	—	`Real` `instLE` `sqrt` `instNatCast` `instAdd` `instOne`	—	`LT.lt.le` `real_sqrt_lt_nat_sqrt_succ`
`real_sqrt_lt_nat_sqrt_succ` 📖	mathematical	—	`Real` `instLT` `sqrt` `instNatCast` `instAdd` `instOne`	—	`sqrt_lt` `instIsOrderedRing` `Nat.cast_zero` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `Nat.lt_succ_sqrt'`
`sq_le` 📖	mathematical	`Real` `instLE` `instZero`	`Monoid.toNatPow` `instMonoid` `instNeg` `sqrt`	—	`instIsOrderedAddMonoid` `abs_le_sqrt` `abs_le` `sq_abs` `le_sqrt` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`sq_lt` 📖	mathematical	—	`Real` `instLT` `Monoid.toNatPow` `instMonoid` `instNeg` `sqrt`	—	`abs_lt` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `sq_abs` `lt_sqrt` `abs_nonneg`
`sq_sqrt` 📖	mathematical	`Real` `instLE` `instZero`	`Monoid.toNatPow` `instMonoid` `sqrt`	—	`sq` `mul_self_sqrt`
`sq_sqrt'` 📖	mathematical	—	`Real` `Monoid.toNatPow` `instMonoid` `sqrt` `instMax` `instZero`	—	`lt_trichotomy`
`sqrt_div` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`division_def` `sqrt_mul` `sqrt_inv`
`sqrt_div'` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`division_def` `sqrt_mul'` `inv_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `sqrt_inv`
`sqrt_div_self` 📖	mathematical	—	`Real` `DivInvMonoid.toDiv` `instDivInvMonoid` `sqrt` `instInv`	—	`sqrt_div_self'` `one_div`
`sqrt_div_self'` 📖	mathematical	—	`Real` `DivInvMonoid.toDiv` `instDivInvMonoid` `sqrt` `instOne`	—	`div_sqrt` `one_div_div`
`sqrt_eq_cases` 📖	mathematical	—	`sqrt` `Real` `instMul` `instLE` `instZero` `instLT`	—	`le_or_gt` `mul_self_sqrt` `sqrt_nonneg` `sqrt_eq_zero_of_nonpos` `LT.lt.le` `sqrt_mul_self`
`sqrt_eq_iff_eq_sq` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt` `Monoid.toNatPow` `instMonoid`	—	`sq` `sqrt_eq_iff_mul_self_eq`
`sqrt_eq_iff_mul_self_eq` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt` `instMul`	—	`mul_self_sqrt` `sqrt_mul_self`
`sqrt_eq_iff_mul_self_eq_of_pos` 📖	mathematical	`Real` `instLT` `instZero`	`sqrt` `instMul`	—	`LT.lt.le` `LT.lt.ne'`
`sqrt_eq_one` 📖	mathematical	—	`sqrt` `Real` `instOne`	—	`sqrt_eq_iff_mul_self_eq_of_pos` `zero_lt_one` `instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `instIsStrictOrderedRing` `mul_one`
`sqrt_eq_zero` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt`	—	`sqrt_zero` `le_rfl`
`sqrt_eq_zero'` 📖	mathematical	—	`sqrt` `Real` `instZero` `instLE`	—	`sqrt.eq_1` `NNReal.coe_eq_zero` `NNReal.sqrt_eq_zero` `toNNReal_eq_zero`
`sqrt_eq_zero_of_nonpos` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt`	—	`sqrt.eq_1` `toNNReal_eq_zero` `NNReal.sqrt_zero`
`sqrt_inj` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt`	—	—
`sqrt_inv` 📖	mathematical	—	`sqrt` `Real` `instInv`	—	`sqrt.eq_1` `toNNReal_inv` `NNReal.sqrt_inv` `NNReal.coe_inv`
`sqrt_le_iff` 📖	mathematical	—	`Real` `instLE` `sqrt` `instZero` `Monoid.toNatPow` `instMonoid`	—	`LE.le.trans` `sqrt_nonneg` `sqrt_le_left`
`sqrt_le_left` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt` `Monoid.toNatPow` `instMonoid`	—	`sqrt.eq_1` `le_toNNReal_iff_coe_le` `NNReal.sqrt_le_iff_le_sq` `sq` `toNNReal_mul` `toNNReal_le_toNNReal_iff` `mul_self_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`sqrt_le_one` 📖	mathematical	—	`Real` `instLE` `sqrt` `instOne`	—	`sqrt_one` `sqrt_le_sqrt_iff` `zero_le_one` `instZeroLEOneClass`
`sqrt_le_sqrt` 📖	mathematical	`Real` `instLE`	`sqrt`	—	`sqrt.eq_1` `NNReal.coe_le_coe` `NNReal.sqrt_le_sqrt` `toNNReal_le_toNNReal`
`sqrt_le_sqrt_iff` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt`	—	`sqrt.eq_1` `NNReal.coe_le_coe` `NNReal.sqrt_le_sqrt` `toNNReal_le_toNNReal_iff`
`sqrt_le_sqrt_iff'` 📖	mathematical	`Real` `instLT` `instZero`	`instLE` `sqrt`	—	`le_total` `LT.lt.not_ge` `Eq.trans_lt` `sqrt_eq_zero_of_nonpos` `sqrt_pos` `LE.le.trans_lt` `sqrt_le_sqrt_iff`
`sqrt_lt` 📖	mathematical	`Real` `instLE` `instZero`	`instLT` `sqrt` `Monoid.toNatPow` `instMonoid`	—	`sqrt_lt_sqrt_iff` `sqrt_sq`
`sqrt_lt'` 📖	mathematical	`Real` `instLT` `instZero`	`sqrt` `Monoid.toNatPow` `instMonoid`	—	`sqrt_lt_sqrt_iff_of_pos` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `instZeroLEOneClass` `sqrt_sq` `LT.lt.le`
`sqrt_lt_sqrt` 📖	mathematical	`Real` `instLE` `instZero` `instLT`	`sqrt`	—	`sqrt_lt_sqrt_iff`
`sqrt_lt_sqrt_iff` 📖	mathematical	`Real` `instLE` `instZero`	`instLT` `sqrt`	—	`lt_iff_lt_of_le_iff_le` `sqrt_le_sqrt_iff`
`sqrt_lt_sqrt_iff_of_pos` 📖	mathematical	`Real` `instLT` `instZero`	`sqrt`	—	`sqrt.eq_1` `NNReal.coe_lt_coe` `NNReal.sqrt_lt_sqrt` `toNNReal_lt_toNNReal_iff`
`sqrt_monotone` 📖	mathematical	—	`Monotone` `Real` `instPreorder` `sqrt`	—	`sqrt_le_sqrt`
`sqrt_mul` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt` `instMul`	—	`sqrt.eq_1` `toNNReal_mul` `NNReal.sqrt_mul`
`sqrt_mul'` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt` `instMul`	—	`mul_comm` `sqrt_mul`
`sqrt_mul_self` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt` `instMul`	—	`mul_self_inj_of_nonneg` `IsStrictOrderedRing.noZeroDivisors` `instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `sqrt_nonneg` `mul_self_sqrt` `mul_self_nonneg` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`sqrt_mul_self_eq_abs` 📖	mathematical	—	`sqrt` `Real` `instMul` `abs` `lattice` `instAddGroup`	—	`abs_mul_abs_self` `sqrt_mul_self` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`sqrt_ne_zero` 📖	—	`Real` `instLE` `instZero`	—	—	`not_iff_not` `sqrt_eq_zero`
`sqrt_ne_zero'` 📖	mathematical	—	`Real` `instLT` `instZero`	—	`not_le` `not_iff_not` `sqrt_eq_zero'`
`sqrt_nonneg` 📖	mathematical	—	`Real` `instLE` `instZero` `sqrt`	—	`NNReal.coe_nonneg`
`sqrt_one` 📖	mathematical	—	`sqrt` `Real` `instOne`	—	`sqrt.eq_1` `toNNReal_one` `NNReal.sqrt_one`
`sqrt_one_add_le` 📖	mathematical	`Real` `instLE` `instNeg` `instOne`	`sqrt` `instAdd` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sqrt_le_iff` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_neg` `instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `neg_neg_of_pos` `instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `instIsOrderedRing` `CancelDenoms.sub_subst` `CancelDenoms.add_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Meta.NormNum.isNat_lt_true` `le_add_of_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Meta.NormNum.isNNRat_pow` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Meta.NormNum.one_natPow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isNNRat_add`
`sqrt_pos` 📖	mathematical	—	`Real` `instLT` `instZero` `sqrt`	—	`lt_iff_lt_of_le_iff_le` `sqrt_eq_zero'`
`sqrt_pos_of_pos` 📖	mathematical	`Real` `instLT` `instZero`	`sqrt`	—	`sqrt_pos`
`sqrt_prod` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt` `Finset.prod` `instCommMonoid`	—	`NNReal.sqrt_zero` `NNReal.sqrt_one` `NNReal.sqrt_mul` `Finset.prod_congr` `coe_sqrt` `NNReal.coe_prod` `sup_of_le_left` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`
`sqrt_sq` 📖	mathematical	`Real` `instLE` `instZero`	`sqrt` `Monoid.toNatPow` `instMonoid`	—	`sq` `sqrt_mul_self`
`sqrt_sq_eq_abs` 📖	mathematical	—	`sqrt` `Real` `Monoid.toNatPow` `instMonoid` `abs` `lattice` `instAddGroup`	—	`sq` `sqrt_mul_self_eq_abs`
`sqrt_two_lt_three_halves` 📖	mathematical	—	`Real` `instLT` `sqrt` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `sq_lt_sq₀` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `instIsOrderedRing` `le_of_lt` `sqrt_pos_of_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE`
`sqrt_zero` 📖	mathematical	—	`sqrt` `Real` `instZero`	—	`sqrt.eq_1` `toNNReal_zero` `NNReal.sqrt_zero`
`strictMonoOn_sqrt` 📖	mathematical	—	`StrictMonoOn` `Real` `instPreorder` `sqrt` `Set.Ici` `instZero`	—	`sqrt_lt_sqrt_iff`
`sum_mul_le_sqrt_mul_sqrt` 📖	mathematical	—	`Real` `instLE` `Finset.sum` `instAddCommMonoid` `instMul` `sqrt` `Monoid.toNatPow` `instMonoid`	—	`LE.le.trans_eq` `le_sqrt_of_sq_le` `Finset.sum_mul_sq_le_sq_mul_sq` `instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `sqrt_mul` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `even_two_mul`
`sum_sqrt_mul_sqrt_le` 📖	mathematical	`Real` `instLE` `instZero`	`Finset.sum` `instAddCommMonoid` `instMul` `sqrt`	—	`Finset.sum_congr` `sq_sqrt` `sum_mul_le_sqrt_mul_sqrt`
`tendsto_sqrt_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `sqrt` `Filter.atTop` `instPreorder`	—	`Eq.le` `map_sqrt_atTop`

---

← Back to Index