Basic

📁 Source: Mathlib/NumberTheory/DiophantineApproximation/Basic.lean

Statistics

Metric	Count
Definitions Ass, convergent	2
Theorems den_le_and_le_num_le_of_sub_lt_one_div_den_sq, finite_rat_abs_sub_lt_one_div_den_sq, convergent_of_int, convergent_of_zero, convergent_succ, convergent_zero, exists_int_int_abs_mul_sub_le, exists_nat_abs_mul_sub_round_le, exists_rat_abs_sub_le_and_den_le, exists_rat_abs_sub_lt_and_lt_of_irrational, exists_rat_eq_convergent, exists_rat_eq_convergent', infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational, infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational	14
Total	16

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
den_le_and_le_num_le_of_sub_lt_one_div_den_sq 📖	mathematical	abs instLattice addGroup Monoid.toNatPow monoid	Int.ceil DivisionRing.toRing instDivisionRing linearOrder instFloorRing Int.floor	—	Nat.cast_pos IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing nontrivial pos mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass LT.lt.ne' div_mul sq abs_of_pos instAddLeftMono abs_mul sub_mul mul_den_eq_num mul_lt_mul_iff_left₀ IsStrictOrderedRing.toMulPosStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE eq_or_ne le_rfl Nat.cast_le instZeroLEOneClass instCharZero LT.lt.le one_lt_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono lt_of_le_of_lt Nat.cast_one Int.cast_natCast Int.cast_one NeZero.charZero_one mul_comm Int.one_le_abs sub_ne_zero_of_ne eq_iff_mul_eq_mul mul_one div_mul_comm div_lt_iff₀ abs_div div_sub' div_mul_eq_mul_div num_div_den abs_sub_lt_iff instIsOrderedAddMonoid LT.lt.trans_le one_div_le zero_lt_one one_div_one sub_le_iff_le_add covariant_swap_add_of_covariant_add Int.instAddLeftMono Int.ceil_le add_comm sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd Int.le_floor
finite_rat_abs_sub_lt_one_div_den_sq 📖	mathematical	—	Set.Finite setOf abs instLattice addGroup Monoid.toNatPow monoid	—	num_div_den den_le_and_le_num_le_of_sub_lt_one_div_den_sq Set.mem_Ioc pos Set.prod_singleton Set.Finite.of_finite_image Set.Finite.subset Set.Finite.biUnion Set.finite_Ioc Set.Finite.prod Set.finite_Icc Set.finite_singleton Function.Injective.injOn

Real

Definitions

Name	Category	Theorems
convergent 📖	CompOp	7 math math: convergent_succ, convergent_of_zero, convergent_zero, exists_rat_eq_convergent, convs_eq_convergent, convergent_of_int, exists_rat_eq_convergent'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convergent_of_int 📖	mathematical	—	convergent Real instIntCast	—	Int.floor_intCast instIsStrictOrderedRing Int.fract_intCast inv_zero convergent_of_zero add_zero
convergent_of_zero 📖	mathematical	—	convergent Real instZero	—	Int.floor_zero instIsStrictOrderedRing Int.cast_zero Int.fract_zero inv_zero add_zero
convergent_succ 📖	mathematical	—	convergent Int.floor Real instRing linearOrder instFloorRing instInv Int.fract	—	—
convergent_zero 📖	mathematical	—	convergent Int.floor Real instRing linearOrder instFloorRing	—	—
exists_int_int_abs_mul_sub_le 📖	mathematical	—	Real instLE abs lattice instAddGroup instSub instMul instIntCast DivInvMonoid.toDiv instDivInvMonoid instOne instAdd instNatCast	—	Nat.cast_zero Nat.cast_one IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass IsStrictOrderedRing.toCharZero instIsStrictOrderedRing mul_lt_of_lt_one_left IsStrictOrderedRing.toMulPosStrictMono Int.fract_lt_one mul_comm le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE abs_of_pos abs_mul instIsOrderedRing Int.floor_le Int.cast_zero MulZeroClass.mul_zero Int.fract_zero MulZeroClass.zero_mul Int.floor_zero Ne.lt_of_le LT.lt.ne Int.instCharZero Finset.mem_Icc Int.cast_add sub_sub sub_mul Int.cast_one one_mul abs_le le_sub_iff_add_le covariant_swap_add_of_covariant_add neg_add_cancel_comm_assoc sub_le_iff_le_add le_of_lt LT.lt.trans lt_one_add NeZero.charZero_one IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd Int.card_Icc Int.card_Ico lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.instIsOrderedAddMonoid Int.floor_lt Int.cast_natCast Finset.mem_Ico Int.floor_nonneg mul_nonneg IsOrderedRing.toPosMulMono Int.fract_nonneg LT.lt.le Mathlib.Tactic.Push.not_and_eq Finset.exists_ne_map_eq_of_card_lt_of_maps_to lt_trichotomy sub_pos_of_lt Int.instAddLeftMono le_add_of_le_of_nonneg Int.cast_sub Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Int.abs_sub_lt_one_of_floor_eq_floor
exists_nat_abs_mul_sub_round_le 📖	mathematical	—	Real instLE abs lattice instAddGroup instSub instMul instNatCast instIntCast round instRing linearOrder instFloorRing DivInvMonoid.toDiv instDivInvMonoid instOne instAdd	—	exists_int_int_abs_mul_sub_le LT.lt.le Nat.cast_le Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero LE.le.trans round_le instIsStrictOrderedRing
exists_rat_abs_sub_le_and_den_le 📖	mathematical	—	Real instLE abs lattice instAddGroup instSub instRatCast DivInvMonoid.toDiv instDivInvMonoid instOne instMul instAdd instNatCast	—	exists_int_int_abs_mul_sub_le Int.cast_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Rat.intCast_div_eq_divInt Rat.den_dvd div_div le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.cast_pos instIsOrderedRing instNontrivial Rat.pos LE.le.trans mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Int.cast_le abs_nonneg covariant_swap_add_of_covariant_add abs_of_pos Rat.cast_div Rat.cast_intCast abs_mul sub_mul div_mul_cancel₀ LT.lt.ne' mul_comm Nat.cast_le Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero
exists_rat_abs_sub_lt_and_lt_of_irrational 📖	mathematical	Irrational	Real instLT abs lattice instAddGroup instSub instRatCast DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow instMonoid instNatCast	—	abs_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sub_ne_zero Irrational.ne_rat exists_nat_gt instIsStrictOrderedRing instArchimedean LT.lt.trans one_div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono exists_rat_abs_sub_le_and_den_le Nat.cast_pos instIsOrderedRing instNontrivial Rat.pos mul_pos add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd zero_lt_one instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero lt_of_le_of_lt sq one_div_lt_one_div mul_lt_mul_iff_left₀ IsStrictOrderedRing.toMulPosStrictMono MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE lt_add_of_le_of_pos Nat.cast_le one_div_lt lt_of_lt_of_le lt_add_one le_mul_iff_one_le_right IsOrderedRing.toPosMulMono Nat.cast_one
exists_rat_eq_convergent 📖	mathematical	Real instLT abs lattice instAddGroup instSub instRatCast DivInvMonoid.toDiv instDivInvMonoid instOne instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow instMonoid	convergent	—	Nat.instAtLeastTwoHAddOfNat exists_rat_eq_convergent' Int.isCoprime_iff_nat_coprime Nat.cast_one one_pow mul_one abs_lt IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Rat.den_eq_one_iff Nat.cast_eq_one Int.instCharZero Nat.cast_pos IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.instNontrivial Rat.pos mul_pos IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing zero_lt_two instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Int.cast_natCast Rat.instCharZero Rat.num_div_den LT.lt.trans one_div sq one_div_lt_one_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul 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.mul_one Mathlib.Tactic.Ring.sub_pf 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_mul Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one add_zero
exists_rat_eq_convergent' 📖	mathematical	ContfracLegendre.Ass	convergent	—	Nat.strong_induction_on lt_trichotomy lt_irrefl LE.le.trans_lt abs_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Nat.cast_zero Int.cast_zero div_zero tsub_zero AddGroup.toOrderedSub MulZeroClass.zero_mul inv_zero Nat.cast_one div_one le_or_gt convergent_zero Int.floor_eq_iff Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.instAtLeastTwo sub_lt_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd abs_lt lt_sub_iff_add_lt' Int.cast_sub Int.cast_one sub_add_cancel LT.lt.le LT.lt.trans Nat.instAtLeastTwoHAddOfNat sub_lt_sub_iff_left IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd one_half_lt_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono eq_or_ne sub_eq_add_neg le_inv_comm₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono zero_lt_one instZeroLEOneClass NeZero.charZero_one Int.fract_pos inv_one one_add_one_eq_two inv_lt_comm₀ zero_lt_two Int.fract_lt_one Int.fract.eq_1 sub_add Mathlib.Meta.NormNum.IsRat.neg_to_eq Mathlib.Meta.NormNum.isRat_neg Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Nat.cast_le Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero LT.lt.ne' Nat.cast_pos IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing Rat.nontrivial Nat.instZeroLEOneClass convergent_succ Int.cast_natCast Rat.instCharZero inv_div sub_div mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass add_sub_cancel
infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational 📖	mathematical	—	Set.Infinite setOf Real instLT abs lattice instAddGroup instSub instRatCast DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow instMonoid instNatCast Irrational	—	irrational_iff_ne_rational Mathlib.Tactic.Contrapose.contrapose₃ Rat.cast_div IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Rat.cast_one Rat.cast_pow Rat.cast_natCast Nat.cast_one Rat.instCharZero Rat.finite_rat_abs_sub_lt_one_div_den_sq infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational
infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational 📖	mathematical	Irrational	Set.Infinite setOf Real instLT abs lattice instAddGroup instSub instRatCast DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow instMonoid instNatCast	—	Set.finite_or_infinite Set.exists_min_image one_div Rat.cast_intCast abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instIsStrictOrderedRing Nat.cast_one one_pow inv_one exists_rat_abs_sub_lt_and_lt_of_irrational lt_irrefl lt_of_le_of_lt

Real.ContfracLegendre

Definitions

Name	Category	Theorems
Ass 📖	MathDef	—

---

← Back to Index