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 📖	mathematical	Real Real.instLE Real.instOne Real.instLT Real.instZero Dist.dist PseudoMetricSpace.toDist Real.instMul	Real Real.instLT Real.instZero Real.instLE Real.instOne Real.instMul Dist.dist PseudoMetricSpace.toDist	—	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 Int.instSemiring algebraMap Int.instCommSemiring Ring.toIntAlgebra Real.instRing Real.instZero	Real Real.instLT Real.instZero Real.instLE Real.instOne Real.instMul Monoid.toPow 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid 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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid 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