Defs

📁 Source: Mathlib/Data/Rat/NatSqrt/Defs.lean

Statistics

Metric	Count
Definitions ratSqrt	1
Theorems lt_ratSqrt_add_inv_prec_sq, ratSqrt_nonneg, ratSqrt_sq_le	3
Total	4

Nat

Definitions

Name	Category	Theorems
ratSqrt 📖	CompOp	7 math math: ratSqrt_sq_le, ratSqrt_nonneg, realSqrt_mem_Ico, realSqrt_lt_ratSqrt_add_inv_prec, lt_ratSqrt_add_inv_prec_sq, ratSqrt_mem_Ioc, ratSqrt_le_realSqrt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lt_ratSqrt_add_inv_prec_sq 📖	mathematical	—	Monoid.toNatPow Rat.monoid ratSqrt	—	mul_lt_mul_iff_of_pos_right IsStrictOrderedRing.toMulPosStrictMono Rat.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass cast_pos' Rat.instAddLeftMono Rat.instZeroLEOneClass NeZero.one Rat.nontrivial mul_pow add_mul Distrib.rightDistribClass div_mul_cancel₀ cast_zero Rat.instCharZero ne_of_gt cast_one lt_succ_sqrt'
ratSqrt_nonneg 📖	mathematical	—	ratSqrt	—	div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Rat.instIsStrictOrderedRing cast_nonneg' Rat.instAddLeftMono Rat.instZeroLEOneClass
ratSqrt_sq_le 📖	mathematical	—	Monoid.toNatPow Rat.monoid ratSqrt	—	div_pow div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Rat.instIsStrictOrderedRing pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass cast_pos' Rat.instAddLeftMono Rat.instZeroLEOneClass NeZero.one Rat.nontrivial Rat.instCharZero sqrt_le'

---

← Back to Index