Basic

📁 Source: Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_one_le_pow_mul_dist, exists_pos_real_of_irrational_root, irrational, transcendental	4
Total	4

Liouville

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_one_le_pow_mul_dist 📖	—	Real Real.instLE Real.instOne Real.instLT Real.instZero Dist.dist PseudoMetricSpace.toDist Real.instMul	—	—	lt_max_iff one_div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing one_le_mul_of_one_le_of_one_le Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing Metric.mem_closedBall' le_trans le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono LT.lt.le not_le one_div_le le_max_left LE.le.trans mul_le_mul_of_nonneg_left le_max_right dist_nonneg zero_le_one
exists_pos_real_of_irrational_root 📖	mathematical	Irrational Polynomial.eval Real Real.semiring Polynomial.map CommSemiring.toSemiring Int.instCommSemiring algebraMap Ring.toIntAlgebra Real.instRing Real.instZero	Real.instLT Real.instLE Real.instOne Real.instMul Monoid.toNatPow Real.instMonoid Real.instAdd Real.instNatCast Polynomial.natDegree Int.instSemiring abs Real.lattice Real.instAddGroup Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid Real.instIntCast	—	Real.instIsDomain Finset.mem_coe Multiset.mem_toFinset Polynomial.mem_roots Polynomial.map_injective RCLike.charZero_rclike Polynomial.map_zero Polynomial.IsRoot.def Metric.exists_closedBall_inter_eq_singleton_of_discrete Set.Finite.isDiscrete T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal Set.toFinite Finite.of_fintype IsCompact.exists_isMaxOn instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid CompactIccSpace.isCompact_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace LT.lt.le sub_lt_self IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono lt_add_of_pos_right Continuous.continuousOn Continuous.comp continuous_abs Polynomial.continuous_aeval IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal exists_one_le_pow_mul_dist one_le_pow₀ Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_add_iff_nonneg_left covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.cast_nonneg mul_comm Convex.norm_image_sub_le_of_norm_deriv_le Polynomial.differentiableAt Polynomial.deriv convex_Icc IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing Real.closedBall_eq_Icc Set.mem_Icc_iff_abs_le Metric.mem_closedBall_self le_of_lt zero_sub abs_neg Nat.cast_one Nat.cast_add Int.cast_add Int.cast_natCast Int.cast_one Int.instCharZero one_le_pow_mul_abs_eval_div Irrational.ne_rational Set.mem_singleton_iff Eq.subset Set.instReflSubset
irrational 📖	mathematical	Liouville	Irrational	—	Rat.cast_mk' Int.cast_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike LT.lt.trans zero_lt_one Int.instZeroLEOneClass Nat.cast_ne_zero mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Ne.bot_lt Int.cast_natCast one_mul abs_of_pos div_lt_div_iff₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE abs_pos LT.lt.ne' pow_pos abs_div div_sub_div Nat.cast_zero Int.cast_zero sub_eq_zero mul_comm div_eq_div_iff CanLift.prf instCanLiftIntNatCastLeOfNat LT.lt.le Int.instAddLeftMono abs_nonneg covariant_swap_add_of_covariant_add not_le Int.instCharZero Nat.cast_one
transcendental 📖	mathematical	Liouville	Transcendental Real Int.instCommRing Real.instRing Ring.toIntAlgebra	—	Polynomial.eval_map_algebraMap exists_pos_real_of_irrational_root irrational pow_unbounded_of_one_lt Real.instIsStrictOrderedRing Real.instArchimedean AddGroup.existsAddOfLE lt_add_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.trans zero_lt_one Int.cast_one Int.cast_lt lt_irrefl LT.lt.trans_le lt_div_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono lt_of_le_of_lt mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing LE.le.trans LT.lt.le Nat.instAtLeastTwoHAddOfNat one_add_one_eq_two pow_le_pow_left₀ IsOrderedRing.toPosMulMono le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Int.cast_ofNat mul_nonneg pow_pos IsStrictOrderedRing.toZeroLEOneClass Int.cast_pos IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass NeZero.one lt_trans IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.instNontrivial abs_nonneg covariant_swap_add_of_covariant_add mul_assoc pow_add CanLift.prf instCanLiftIntNatCastLeOfNat zero_le_one Int.instZeroLEOneClass div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.instZeroLEOneClass Nat.cast_succ

---

← Back to Index