GoldenRatio

📁 Source: Mathlib/NumberTheory/Real/GoldenRatio.lean

Statistics

Metric	Count
Definitions fibRec, goldenConj, goldenRatio, termφ, termψ	5
Theorems coe_fib_eq, coe_fib_eq', coe_intFib_eq, fibRec_charPoly_eq, fib_isSol_fibRec, fib_succ_sub_goldenConj_mul_fib, fib_succ_sub_goldenRatio_mul_fib, geom_goldenConj_isSol_fibRec, geom_goldenRatio_isSol_fibRec, goldenConj_irrational, goldenConj_mul_fib_succ_add_fib, goldenConj_mul_goldenRatio, goldenConj_ne_zero, goldenConj_neg, goldenConj_sq, goldenRatio_add_goldenConj, goldenRatio_irrational, goldenRatio_lt_two, goldenRatio_mul_fib_succ_add_fib, goldenRatio_mul_goldenConj, goldenRatio_ne_zero, goldenRatio_pos, goldenRatio_pow_sub_goldenRatio_pow, goldenRatio_sq, goldenRatio_sub_goldenConj, inv_goldenConj, inv_goldenRatio, neg_one_lt_goldenConj, one_lt_goldenRatio, one_sub_goldenConj, one_sub_goldenRatio	31
Total	36

Real

Definitions

Name	Category	Theorems
fibRec 📖	CompOp	4 math math: geom_goldenRatio_isSol_fibRec, fibRec_charPoly_eq, fib_isSol_fibRec, geom_goldenConj_isSol_fibRec
goldenConj 📖	CompOp	21 math math: goldenConj_irrational, goldenConj_mul_fib_succ_add_fib, goldenRatio_mul_goldenConj, inv_goldenConj, inv_goldenRatio, neg_one_lt_goldenConj, coe_fib_eq, goldenConj_mul_goldenRatio, Finset.doubling_lt_golden_ratio, coe_intFib_eq, tendsto_fib_div_fib_succ_atTop, goldenConj_neg, goldenRatio_add_goldenConj, one_sub_goldenConj, goldenConj_sq, coe_fib_eq', goldenRatio_sub_goldenConj, fib_succ_sub_goldenConj_mul_fib, fib_succ_sub_goldenRatio_mul_fib, one_sub_goldenRatio, geom_goldenConj_isSol_fibRec
goldenRatio 📖	CompOp	23 math math: geom_goldenRatio_isSol_fibRec, goldenRatio_mul_goldenConj, goldenRatio_lt_two, inv_goldenConj, inv_goldenRatio, one_lt_goldenRatio, goldenRatio_irrational, goldenRatio_pow_sub_goldenRatio_pow, coe_fib_eq, goldenConj_mul_goldenRatio, goldenRatio_mul_fib_succ_add_fib, Finset.doubling_lt_golden_ratio, coe_intFib_eq, goldenRatio_add_goldenConj, goldenRatio_pos, one_sub_goldenConj, coe_fib_eq', tendsto_fib_succ_div_fib_atTop, goldenRatio_sub_goldenConj, fib_succ_sub_goldenConj_mul_fib, fib_succ_sub_goldenRatio_mul_fib, one_sub_goldenRatio, goldenRatio_sq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_fib_eq 📖	mathematical	—	Real instNatCast Nat.fib DivInvMonoid.toDiv instDivInvMonoid instSub Monoid.toPow instMonoid goldenRatio goldenConj sqrt instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat coe_fib_eq'
coe_fib_eq' 📖	mathematical	—	Real instNatCast Nat.fib DivInvMonoid.toDiv instDivInvMonoid instSub Monoid.toPow instMonoid goldenRatio goldenConj sqrt instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat LinearRecurrence.sol_eq_of_eq_init fib_isSol_fibRec Submodule.sub_mem Submodule.smul_mem geom_goldenRatio_isSol_fibRec geom_goldenConj_isSol_fibRec Pi.sub_apply Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_atom Mathlib.Tactic.Ring.pow_zero 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.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr CharP.cast_eq_zero CharP.ofCharZero pow_zero sub_self zero_div pow_one goldenRatio_sub_goldenConj div_self instIsOrderedRing
coe_intFib_eq 📖	mathematical	—	Real instIntCast Int.fib DivInvMonoid.toDiv instDivInvMonoid instSub DivInvMonoid.toZPow goldenRatio goldenConj sqrt instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat coe_fib_eq Int.fib_neg Int.cast_ite Int.cast_neg Int.cast_natCast zpow_neg zpow_natCast inv_goldenRatio neg_one_mul mul_pow neg_one_pow_eq_ite inv_goldenConj
fibRec_charPoly_eq 📖	mathematical	—	LinearRecurrence.charPoly fibRec CommRing.toCommSemiring Polynomial CommSemiring.toSemiring Polynomial.instSub CommRing.toRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Polynomial.instAdd Polynomial.instOne	—	fibRec.eq_1 LinearRecurrence.charPoly.eq_1 one_smul Finset.sum_congr Finset.sum_fin_eq_sum_range Nat.instNoMaxOrder Finset.sum_range_succ' covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd Matrix.cons_val_succ' Matrix.cons_val_fin_one Finset.sum_ite_eq' zero_add pow_one pow_zero
fib_isSol_fibRec 📖	mathematical	—	LinearRecurrence.IsSolution fibRec AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring Nat.fib	—	fibRec.eq_1 Finset.sum_congr Nat.fib_add_two add_comm Nat.cast_add Finset.sum_fin_eq_sum_range Nat.instNoMaxOrder Finset.sum_range_succ' covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd Matrix.cons_val_succ' Matrix.cons_val_fin_one one_mul Finset.sum_ite_eq' zero_add add_zero
fib_succ_sub_goldenConj_mul_fib 📖	mathematical	—	Real instSub instNatCast Nat.fib instMul goldenConj Monoid.toPow instMonoid goldenRatio	—	—
fib_succ_sub_goldenRatio_mul_fib 📖	mathematical	—	Real instSub instNatCast Nat.fib instMul goldenRatio Monoid.toPow instMonoid goldenConj	—	Nat.instAtLeastTwoHAddOfNat coe_fib_eq mul_div div_sub_div_same mul_sub pow_succ' Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_atom Mathlib.Tactic.Ring.pow_zero 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_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.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Tactic.Ring.inv_mul Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.RingNF.nnrat_rawCast Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg add_zero mul_one Mathlib.Meta.NormNum.isNat_le_true instIsOrderedRing Nat.cast_zero Mathlib.Meta.NormNum.isNat_eq_false mul_inv_cancel₀ one_mul
geom_goldenConj_isSol_fibRec 📖	mathematical	—	LinearRecurrence.IsSolution Real instCommSemiring fibRec Monoid.toPow instMonoid goldenConj	—	LinearRecurrence.geom_sol_iff_root_charPoly fibRec_charPoly_eq Polynomial.eval_sub Polynomial.eval_pow Polynomial.eval_X goldenConj_sq Polynomial.eval_add Polynomial.eval_one sub_self
geom_goldenRatio_isSol_fibRec 📖	mathematical	—	LinearRecurrence.IsSolution Real instCommSemiring fibRec Monoid.toPow instMonoid goldenRatio	—	LinearRecurrence.geom_sol_iff_root_charPoly fibRec_charPoly_eq Polynomial.eval_sub Polynomial.eval_pow Polynomial.eval_X goldenRatio_sq Polynomial.eval_add Polynomial.eval_one sub_self
goldenConj_irrational 📖	mathematical	—	Irrational goldenConj	—	Nat.Prime.irrational_sqrt Mathlib.Meta.NormNum.isNat_prime_2 Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_minFac_4 Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.minFacHelper_0 Irrational.ratCast_sub Nat.instAtLeastTwoHAddOfNat Rat.cast_ofScientific Rat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one 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.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_nnrat Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.natPow_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Rat.instCharZero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Irrational.ratCast_mul Mathlib.Meta.NormNum.isNNRat_eq_false
goldenConj_mul_fib_succ_add_fib 📖	mathematical	—	Real instAdd instMul goldenConj instNatCast Nat.fib Monoid.toPow instMonoid	—	—
goldenConj_mul_goldenRatio 📖	mathematical	—	Real instMul goldenConj goldenRatio instNeg instOne	—	mul_comm goldenRatio_mul_goldenConj
goldenConj_ne_zero 📖	—	—	—	—	ne_of_lt goldenConj_neg
goldenConj_neg 📖	mathematical	—	Real instLT goldenConj instZero	—	lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one 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.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isRat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.le_of_le_of_eq Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing neg_eq_zero sub_eq_zero_of_eq one_sub_goldenConj Mathlib.Tactic.Linarith.sub_neg_of_lt one_lt_goldenRatio
goldenConj_sq 📖	mathematical	—	Real Monoid.toPow instMonoid goldenConj instAdd instOne	—	—
goldenRatio_add_goldenConj 📖	mathematical	—	Real instAdd goldenRatio goldenConj instOne	—	goldenRatio.eq_1 goldenConj.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr 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.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz
goldenRatio_irrational 📖	mathematical	—	Irrational goldenRatio	—	Nat.Prime.irrational_sqrt Mathlib.Meta.NormNum.isNat_prime_2 Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_minFac_4 Mathlib.Meta.NormNum.IsNat.raw_refl Mathlib.Meta.NormNum.minFacHelper_0 Irrational.ratCast_add Nat.instAtLeastTwoHAddOfNat Rat.cast_ofScientific Rat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_nnrat Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true Mathlib.Meta.NormNum.isNNRat_ratCast Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_mkRat Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.natPow_one Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNat_intCast Mathlib.Meta.NormNum.isNat_intOfNat Rat.instCharZero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Irrational.ratCast_mul Mathlib.Meta.NormNum.isNNRat_eq_false
goldenRatio_lt_two 📖	mathematical	—	Real instLT goldenRatio instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat div_lt_div_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing add_lt_add_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sqrt_lt' Mathlib.Meta.NormNum.isNat_lt_true instIsOrderedRing IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.Positivity.pos_of_isNat instNontrivial Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNat_add Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos
goldenRatio_mul_fib_succ_add_fib 📖	mathematical	—	Real instAdd instMul goldenRatio instNatCast Nat.fib Monoid.toPow instMonoid	—	zero_add Nat.cast_one mul_one CharP.cast_eq_zero CharP.ofCharZero IsStrictOrderedRing.toCharZero instIsStrictOrderedRing add_zero pow_one Nat.fib_add_one Nat.cast_add goldenRatio_sq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.pow_zero add_comm Mathlib.Tactic.Ring.pow_atom
goldenRatio_mul_goldenConj 📖	mathematical	—	Real instMul goldenRatio goldenConj instNeg instOne	—	—
goldenRatio_ne_zero 📖	—	—	—	—	ne_of_gt goldenRatio_pos
goldenRatio_pos 📖	mathematical	—	Real instLT instZero goldenRatio	—	mul_pos IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Mathlib.Meta.NormNum.isNat_lt_true instIsOrderedRing IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE zero_lt_two instZeroLEOneClass NeZero.charZero_one
goldenRatio_pow_sub_goldenRatio_pow 📖	mathematical	—	Real instSub Monoid.toPow instMonoid goldenRatio	—	—
goldenRatio_sq 📖	mathematical	—	Real Monoid.toPow instMonoid goldenRatio instAdd instOne	—	—
goldenRatio_sub_goldenConj 📖	mathematical	—	Real instSub goldenRatio goldenConj sqrt instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Mathlib.Tactic.Ring.of_eq Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul 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.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add
inv_goldenConj 📖	mathematical	—	Real instInv goldenConj instNeg goldenRatio	—	inv_eq_iff_eq_inv neg_inv neg_eq_iff_eq_neg inv_goldenRatio
inv_goldenRatio 📖	mathematical	—	Real instInv goldenRatio instNeg goldenConj	—	—
neg_one_lt_goldenConj 📖	mathematical	—	Real instLT instNeg instOne goldenConj	—	neg_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add inv_goldenRatio inv_lt_one_of_one_lt₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing instZeroLEOneClass one_lt_goldenRatio
one_lt_goldenRatio 📖	mathematical	—	Real instLT instOne goldenRatio	—	lt_of_mul_lt_mul_left PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing mul_one goldenRatio_sq IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_lt_of_covariant_le instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero le_of_lt goldenRatio_pos
one_sub_goldenConj 📖	mathematical	—	Real instSub instOne goldenRatio goldenConj	—	Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing sub_eq_zero_of_eq goldenRatio_add_goldenConj Mathlib.Tactic.Ring.neg_congr neg_eq_zero
one_sub_goldenRatio 📖	mathematical	—	Real instSub instOne goldenConj goldenRatio	—	Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.div_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.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isRat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing sub_eq_zero_of_eq goldenRatio_add_goldenConj Mathlib.Tactic.Ring.neg_congr neg_eq_zero

goldenRatio

Definitions

Name	Category	Theorems
termφ 📖	CompOp	—
termψ 📖	CompOp	—

---

← Back to Index