Documentation Verification Report

RealSqrt

📁 Source: Mathlib/Tactic/NormNum/RealSqrt.lean

Statistics

Metric	Count
Definitions `evalNNRealSqrt`, `evalRealSqrt`	2
Theorems `isNNRat_nnrealSqrt_of_isNNRat`, `isNNRat_realSqrt_of_isNNRat`, `isNat_nnrealSqrt`, `isNat_realSqrt`, `isNat_realSqrt_neg`, `isNat_realSqrt_of_isRat_negOfNat`	6
Total	8

Tactic.NormNum

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNNRat_nnrealSqrt_of_isNNRat` 📖	mathematical	`Mathlib.Meta.NormNum.IsNNRat` `NNReal` `instSemiringNNReal`	`DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `NNReal.sqrt`	—	`mul_self_ne_zero` `NNReal.instNoZeroDivisors` `Nat.cast_mul` `Invertible.ne_zero` `invOf_eq_inv` `mul_inv_rev` `NNReal.sqrt_mul` `NNReal.sqrt_mul_self`
`isNNRat_realSqrt_of_isNNRat` 📖	mathematical	`Mathlib.Meta.NormNum.IsNNRat` `Real` `Real.semiring`	`Real.sqrt`	—	`mul_self_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Nat.cast_mul` `Invertible.ne_zero` `Real.instNontrivial` `invOf_eq_inv` `mul_inv_rev` `Real.sqrt_mul` `mul_self_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.sqrt_mul_self` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono`
`isNat_nnrealSqrt` 📖	mathematical	`Mathlib.Meta.NormNum.IsNat` `NNReal` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instFunLikeOrderIso` `NNReal.sqrt`	—	`Mathlib.Meta.NormNum.IsNat.out` `Nat.cast_mul` `NNReal.sqrt_mul_self`
`isNat_realSqrt` 📖	mathematical	`Mathlib.Meta.NormNum.IsNat` `Real` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.instRing`	`Real.sqrt`	—	`Mathlib.Meta.NormNum.IsNat.out` `Nat.cast_mul` `Real.sqrt_mul_self` `Real.instIsOrderedRing`
`isNat_realSqrt_neg` 📖	mathematical	`Mathlib.Meta.NormNum.IsInt` `Real` `Real.instRing`	`Mathlib.Meta.NormNum.IsNat` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.sqrt`	—	`Mathlib.Meta.NormNum.IsInt.out` `Int.cast_negOfNat` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instIsOrderedRing`
`isNat_realSqrt_of_isRat_negOfNat` 📖	mathematical	`Mathlib.Meta.NormNum.IsRat` `Real` `Real.instRing`	`Mathlib.Meta.NormNum.IsNat` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.sqrt`	—	`mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `invOf_nonneg` `Real.instIsStrictOrderedRing` `Int.cast_negOfNat` `invOf_eq_inv` `neg_mul` `Nat.cast_zero` `Rat.cast_natCast`

---

← Back to Index